In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. (Def: http://en.m.wikipedia.org/wiki/Higher-order_logic)

learn more… | top users | synonyms

0
votes
2answers
37 views

Show that well-ordering is not a first-order property.

Problem description: Show that well-ordering is not a first-order notion. Suppose that $\Gamma$ axiomatizes the class of well-orderings. Add countably many constants $c_i$ and show that $\Gamma \cup ...
0
votes
0answers
28 views

Formalising a problem given in natural language into predicate logic

I am working on a research paper and I want to formalise the problem which we tackle and process for solving it using predicate logic. I used predicate logic in the past for formalising simple ...
0
votes
1answer
62 views

Is mathematical induction the only known example of a higher-order logic?

Mathematical induction is one well known and widely cited example of a second-order logic. I was wondering whether there are other examples of arguments involving higher-order logic in any branch of ...
3
votes
2answers
56 views

Can the transfer principle apply to second-order logic if we transfer sets and relations to hyper-sets and hyper-relations?

The transfer principle doesn't apply to second-order logic. For example, if I take a standard statement. $$\text{A lower bounded set of Reals has a greatest lower bound}$$ Is false for the ...
1
vote
1answer
45 views

Expressive Power of Second-Order Logic vs. Higher-Order Logics

My question regards the expressive power of second-order logic as compared with third-order logic. Throughout, I am working in the standard or full semantics of higher-order logics (so not the Henkin ...
1
vote
3answers
114 views

$\exists x ~ \forall y ~ f(x, y) \iff \forall y() ~ \exists x~ f(x, y(x))$ Name? Proof?

I was looking at potential theorems, and this one came up: $$\bigg(\exists x ~ \forall y ~:~ f(x, y) \bigg) \iff \bigg(\forall y() ~ \exists x ~:~ f(x, y(x))\bigg)$$ (where the second $y$ is ...
2
votes
3answers
62 views

Formulating that the universe is finite without establishing an upper limit

There is a fairly common example of a 2nd order formula that is only true in a universe with infinite domain: $$\begin{align} \exists R \quad & \forall x && \lnot xRx \\ \land ...
0
votes
1answer
41 views

Can monadic second-order logic characterize finiteness?

Is there a monadic second-order (MSO) theory, or even formula, T over some signature $\Sigma$, such that for every structure M for $\Sigma$, M satisfies T if and only if M is finite? (Note that this ...
3
votes
0answers
25 views

Extensionality of a hierarchy of functionals over $\mathbb{N}$

Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. ...
0
votes
3answers
61 views

A course on Logic.

I'm looking for a selection of books, in order to properly learn logic, starting from the most basic principles of propositional calculus and going up the ladder, up to higher order logic. My number ...
1
vote
2answers
103 views

Higher-Order Logic in ordinary Mathematics?

Do we use the language of higher-order logic in ordinary mathematics? (If yes: Can you give some examples?) Or are we always working with first-order logic? Comment: Maybe you are going to say that ...
0
votes
0answers
65 views

Calculating high order moments

All the information I can find about "higher order" moments seems to stop at Kurtosis which is only the 4th moment. What about the 5th, 6th, 7th, etc? I get that the formula is basically the same, but ...
1
vote
0answers
49 views

What logical resources does one need to distinguish $\mathbb{R}\hspace{-0.05 in}-\hspace{-0.04 in}\mathbb{Q}$ from $\mathbb{Q}$?

(I'm inspired by this question.) As a strict lower bound, having just the order relation is not enough, since $\mathbb{R}\hspace{-0.05 in}-\hspace{-0.04 in}\mathbb{Q}$ and $\mathbb{Q}$ are both ...
3
votes
1answer
155 views

How to show incompleteness of second order logic?

I'm trying to see/show that second order logic (with full semantics) is incomplete - i.e. that there are sentences that are true in all models of some theory $T$, and yet still can not be proved from ...
0
votes
2answers
97 views

Sound deductive systems with biggest set of provable sentences in second-order logic?

In second-order logic (with standard semantics), we know that there are sound deductive systems, and we know that no sound deductive system can derive all true statements. I was wondering whether ...
1
vote
1answer
63 views

Axiomatizability in monadic second-order logic

For my thesis in finite model theory I'm considering some basic classes of structures, and I want to show in which logical systems they can or cannot be axiomatized. I now consider the class ...
2
votes
1answer
107 views

Is there a 'largest' second-order categorical axiomatization of set theory, extended from ZFC2

While it's possible to obtain categorical second-order axiomatizations of set theory by extending ZFC2 with additional axioms (see [1]), these axioms seem somewhat arbitrary (e.g. adding an axiom that ...
2
votes
2answers
93 views

Are categorical second-order axiomatizations of set theory inconsistent due to the axiom of replacement

Second-order ZFC is nearly categorical, except that it does not determine the 'height' of the cumulative hierarchy (intuitively speaking). However, additional axioms can be added to second-order ZFC ...
5
votes
1answer
150 views

Is there any formula of monadic second-order logic that is only satisfied by an infinite set?

Is there any formula, of monadic second-order logic, that is only satisfied by an infinite set?
4
votes
1answer
91 views

How high up do kinds go in type theory?

I understand this is a bit naive, but I just learned how types can have types that we call 'kinds,' in system F$\omega$ as a sort of extended higher order lambda calculus. The wiki article on it ...
2
votes
1answer
155 views

Do I really need lambda abstraction for type theory?

So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm ...
0
votes
0answers
49 views

How do we express higher arity predicates and functions in terms of membership?

It's been noted by others that higher order logic is similar to set theory. We can express the second order statement $\forall$R$\forall$x(R(x)) as a first order statement $\forall$R$\forall$x (x ...
2
votes
0answers
37 views

What strongly normalizing lambda calculi exist that can be integrated with/as logic?

If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend ...
1
vote
2answers
194 views

What does a prime (apostrophe) mean before a predicate?

I found this statement in a paper by John McCarthy: $$ \forall x.ostrich\ x \supset species\ x ={}^\prime{}ostrich $$ I can't figure out what the prime indicates.
5
votes
1answer
94 views

Is there a syntax for type quantification in higher order logic?

I'm trying to understand higher order logic deduction, and I sort of understand how after going to third order logic and higher you have a type explosion; predicates and functions can have a large ...
0
votes
0answers
72 views

Are proofs for many-sorted first order logic shorter than single sorted first order logic?

I understand that the expressive power of first order logic with one sort is the same as any many sorted first order logic, and that higher order logic with general semantics is the same as a many ...
6
votes
4answers
527 views

Why aren't valid higher order logic sentences recursively enumerable in full semantics?

It's said (proven in some reduction to the Gödel–Rosser theorem?) that second order logic and higher fails to be complete for full semantics; that is there isn't any semi-algorithm for determining if ...
1
vote
2answers
106 views

For which subsystems T of 2nd order arithmetic is there a model of T + $\neg$Con(T)?

A theory T might have the following property: there is a model of T + $\neg$Con(T) 1st order PA has this property, but full 2nd order PA doesn't. Among subsystems of 2nd order arithmetic, which ones ...
6
votes
2answers
230 views

Defining addition in second order logic

(before saying it's duplicate, read whole question) I was told by someone that we can define addition and multiplication purely in terms of successor function, provided that we work in second order ...
1
vote
0answers
73 views

If full semantics higher order logic is set theory, which set theory is it?

I've been trying to get a handle on how higher order logic interacts with set theory. It's been stated convincingly that higher order logic with full semantics is set theory in sheep's clothing. For ...
2
votes
1answer
68 views

Flattening quantification over relations

I already asked this question in stack overflow here and somebody suggested to post it here. I repeat the question again: I have a Relation f defined as $f: A \to B × C$. I would like to write a ...
1
vote
1answer
130 views

What syntax exists for higher order logic?

I know this is sort of a broad question, but I'm having trouble getting a handle on the syntax for higher order logic, when going from first order logic. Basically I want to be able to do resolution ...
2
votes
1answer
111 views

How is quantifier elimination accomplished in second and higher order logic?

In first order logic we can eliminate existential quantifiers using a second order equivalence relation: $\forall$x$\exists$y P(x, y) $\iff$ $\exists$f$\forall$x P(x, f(x)) Dropping the existential ...
5
votes
2answers
1k views

What are some examples of third, fourth, or fifth order logic sentences?

I know this seems like an obvious question, but I haven't been able to find any examples of sentences in logic higher than second order, so my intuition on how it's supposed to behave is failing me. ...
1
vote
1answer
38 views

higher order ODE convert problem

I have $$y'''- 3\,y'- x\,y = 0.$$ How to convert this to three first order differential equations? I got stuck for using Let $z=y''$
0
votes
1answer
641 views

Can somebody please help me with math problems for 8th grade?

1) Determine if the following statement is true or false. If false, provide a counterexample: "An equation with an integer coefficient will always have an integer solution.". 2) Write a rel-world ...
1
vote
0answers
55 views

Characterizability in $L^2_{\kappa^+\omega}$

I'm reading an article on second order characterizability. At some point in the article it proves that any model $A$ of cardinality $\kappa$ must be characterizable in $L^2_{\kappa^+\omega}$. I.e. ...
2
votes
0answers
131 views

Can “tit for tat” strategy be defined in monadic second-order logic?

Prisoner's dilema game can be represented as a game tree, which could be infinite game with corresponding infinite game (binary) tree in common case. There is well-known tit for tat strategy, which ...
12
votes
2answers
1k views

What's an example of a theory that's consistent yet has no model?

By the completeness theorem for first order logic, if a theory is consistent then it has a model. But what's a counterexample to this : what's an example of a logic where some theory is consistent ...
3
votes
2answers
148 views

Is the first-order incompleteness of a theory (like arithmetics, set theory or logic itself) avoidable in a second or higher-order axiomatizations?

Can we avoid the first-order incompleteness of a theory (like arithmetics or set theory) in a second-order theory which contains the previous? How does it depend on the chosen semantics or models? If ...
1
vote
1answer
53 views

Second order universal quantifier elimination restriction

Dirk van Dalen in his Logic and Structure gives following universal elimination rule: from $\forall_{X^n} \phi$ infer $\phi^*$ where $\phi^*$ is $\phi$ in which every occurence of $X^n(t_1, ..., ...
0
votes
1answer
82 views

What is the difference between logical and iterative set

Saphiro in his "foundations without foundationalism: a case for second-order logic" defends second-order logic by claiming that talking about subsets of domain is not problematic in case of SOL. He ...
0
votes
1answer
113 views

Logic question in Real Analysis

I thought about posting some minor insecurities and some main doubts i have on a particular topic. Let R with the usual metric be a metric space, $A \subseteq R$ , $f:A\to R$ and p is a limit ...
3
votes
2answers
128 views

Are higher order logics substantially stronger than second order

Do we get much by using logics of order higher that 2? Does each transition to next level provides much power?
0
votes
1answer
113 views

Proving property for all predicates in first order logic

Let's consider language with predicate $P$ and following derivation $${{{[P[a/x]]^1} \over {P[a/x] \rightarrow P[a/x]}}\rightarrow I^1 \over {\forall_x (P(x) \rightarrow P(x))}}\forall I$$ Doesn't ...
3
votes
1answer
106 views

Completness in higher order logic and Interpretations

It´s known that for first order theories, it holds $\mathbf{ZFC} \vdash T \vdash \varphi \leftrightarrow T \models \varphi$. Why does this not hold in the higher order case (any simple example?)? ...
1
vote
2answers
123 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
2
votes
2answers
148 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
6
votes
4answers
252 views

Why aren't there any first-order sentences which have the property of being true in all non-standard models of PA and false in the standard one?

I'd like to know where the following result comes from (that is, whether there is a more general result from which it follows or else how it can be proven): There is no first-order sentence which is ...
2
votes
0answers
89 views

A consistent first-order theory whose impredicative second-order variant is inconsistent

Let's assume that we have a consistent first-order theory, which was derived from a second order theory by replacing universal quantification over second order variables by axiom schemes for ...