Timeline for Second-order term in first-order logic?

5 events

when toggle format	what		by	license	comment
Aug 23, 2012 at 7:35	comment	added	Andrej Bauer		@kate_r: The essential thing to graps is that there can be many domains, even infinitely many ones. So you can quantify over any domain you like. In your case the domains would correspond to simple types, so they would be $A \to B$, $(A \to B) \to (A \to B)$, etc., whatever you like. Have a look at $\mathrm{HA}^\omega$, higher-order Heyting arithmetic. It is an example of a first-order theory with arbitrarily complex domains of the form $\mathbb{N} \to \mathbb{N}$, $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, $((\mathbb{N} \to \mathbb{N}) \to \mathbb{N}) \to \mathbb{N}$, etc.
Aug 23, 2012 at 2:32	comment	added	Carl Mummert		I voted for this earlier, but I feel obliged to say I think my answer is just a more detailed explanation of some ideas expressed in this one.
Aug 22, 2012 at 17:14	comment	added	kate_r		Thanks. Just to clarify my understanding: the quantification of variables of type $A \to B$ is valid in FOL because the elements of the domain in question are of type $A \to B$. If so, how come the quantification over $(A \to B) \to (A \to B)$ is still valid in FOL?
Aug 22, 2012 at 16:24	history	edited	Andrej Bauer	CC BY-SA 3.0	added 409 characters in body
Aug 22, 2012 at 16:13	history	answered	Andrej Bauer	CC BY-SA 3.0