1
vote
2answers
92 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 ...
3
votes
2answers
89 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 ...
2
votes
1answer
60 views

Does second-order arithmetic (Z2) prove soundness and uniform reflection for first-order arithmetic (PA)?

(1) Does full second-order arithmetic (Z2) prove soundness and uniform reflection schemas for first-order arithmetic (PA)? That is, do we have for all formulas $\phi$: $$ \underset \phi \forall \; ...
6
votes
2answers
107 views

There is a second-order sentence that is valid in standard semantics but not valid in Henkin semantics?

Let $\Sigma^\mathrm{ST}$ be a set of sentences that is valid in standard semantics and $\Sigma^\mathrm{Henk}$ be a set of sentences that is valid in Henkin semantics. Since ...
1
vote
0answers
37 views

How is it possible that the well-ordering theorem is strictly stronger than the axiom of choice in second-order logic? [duplicate]

If I am not wrong, the well-ordering theorem is strictly stronger than the axiom of choice in second-order logic. I am not sure to understand how this is possible. The reason is that second order ...
3
votes
1answer
88 views

Why is better to work with first-order Peano's axioms than with second-order Peano's axioms?

In the case of Peano's axioms the second-order version is categorical, but the first-order is not. Besides, with the second-order version the operations: addition, multiplication and exponentiation ...
2
votes
1answer
94 views

Why is better to work with first-order logic than with second-order logic? [duplicate]

Why is better to work with first-order logic than with second-order logic? In the case of Peano's axioms the second-order version is categorical, but the first-order is not. Besides, with the ...
2
votes
1answer
135 views

Any “natural” examples of true statements in number theory not provable in 2nd order systems?

I know that there are a few theorems in number theory that are somehow known to be true, but have been shown not to be provable in first-order Peano arithmetic (PA). Have any so-called "natural" ...
4
votes
1answer
85 views

What is the intuition behind $\Delta_1^0$ sets and $\Delta_1^1$ sets?

In the context of first-order arithmetic, if $\phi$ is a formula with only bounded quantifiers, then if you put existential quantifiers in front it becomes a $\Sigma_1^0$ formula according to the ...
2
votes
1answer
43 views

What subsystem of second-order arithmetic can interpret the theory of real closed fields?

Real numbers can be encoded as sets of natural numbers, because they can be encoded as Dedekind cuts or Cauchy sequences of rational numbers, and a rational number can be encoded by a natural number. ...
2
votes
1answer
104 views

Who first proved that the second-order theory of real numbers is categorical?

The second-order theory of real numbers is obtained by taking the axioms of ordered fields and adding a (Dedekind) completeness axiom, which states that every set which has an upper bound has a least ...
1
vote
0answers
52 views

What is the proof-theoretic strength of the predicative second-order theory of real numbers?

The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula ...
5
votes
1answer
77 views

What is $M_x$ in Frege's Basic Law IIb?

Gottlob Frege's magnum opus, "The Basic Laws of Arithmetic" (Die Grundgesetze der Arithmetic in German) constitutes one of most impressive and meticulous attempts at developing a rigorous foundation ...
3
votes
1answer
108 views

Can equinumerosity by defined in monadic second-order logic?

Two properties (or concepts) $F$ and $G$ are said to be equinumerous if they have the same cardinality, i.e. if they can be put in one-to-one correspondence with each other. This can be very easily ...
2
votes
2answers
125 views

Peano arithmetic with the second-order induction axiom

I am in the middle of my PhD and I am trying to reinforce my knowledge of mathematics by studying the foundations of Analysis. The first task is to get the bases of the natural numbers. So for this I ...
4
votes
3answers
196 views

How can one quantify on a function in ZFC?

I have read that $ZFC$ and first-order logic could formalize all the mathematics, but I do not manage to conceive that. First, let me show what my understanding of $ZFC$ is. I have read that $ZFC$ was ...
6
votes
1answer
628 views

Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory

I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain ...
3
votes
3answers
190 views

what are first and second order logics? [duplicate]

The only knowledge I have on logic is due to a book I read a couple of years ago called Introduction to logic: and to the methodology of deductive sciences by Alfred Tarski. And in it he talks about ...
4
votes
2answers
230 views

Do isomorphic structures always satisfy the same second-order sentences?

I know that if two mathematical structures are isomorphic, then they satisfy the same first-order sentences. The converse is false. This is probably a completely obvious question, but is it true that ...
5
votes
2answers
138 views

Henkin vs. “Full” Semantics for Second-order Logic and Multi-Sorted First Order Interpretations

In this paper by Jeff Ketland, he notes: With Henkin semantics, the Completeness, Compactness and Löwenheim-Skolem Theorems all hold, because Henkin structures can be re-interpreted as many-sorted ...
4
votes
2answers
144 views

Is higher order type theory the same as higher order logic?

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types. In mathematical logic we have higher-order ...
11
votes
2answers
292 views

Is second order logic even a logic?

Second order logic is a language, but, is it a logic? My understanding is that a logic (or "logical system") is an ordered pair; it is a formal system together with a semantics. However, the language ...
2
votes
1answer
145 views

Is the expressive power of infinitary logic language $L(\infty,\infty)$ larger, the same or smaller than that of ZFC+large cardinal axioms?

In a previous question I learned that the power of statements of the form $\Pi_m^n$ or $\Sigma_m^n$ for arbitrary positive $m$ and $n$, is smaller than that of ZFC. For instance, the GCH cannot be ...
7
votes
2answers
220 views

Monadic second order logic without constants, functions and equality

Leibniz's law of the identity of indiscernibles can be stated in monadic second order logic: $$\forall x\forall y (x=y \leftarrow \forall P (Px \leftrightarrow Py))$$ This law is true for standard ...
0
votes
1answer
150 views

Are there statements in set theory about arithmetic beyond the reach of the analytical hierarchy?

Even if the answer were negative for arithmetics(I have no idea), in the more general case: Can any mathematical statement be expressed as a $\Delta_m^n$ (with n, m belongs to N) statement in a chosen ...
4
votes
1answer
188 views

Can second order logic express each (computable) infinitary logic sentence?

In chapter 9 of Ebbinghaus et. al, the logical systems $\mathcal{L}_\text{II}$ ("full" second order logic with standard semantics) and $\mathcal{L}_{\omega_1\omega}$ (countable infinitary logic with ...
4
votes
1answer
165 views

Is every φ above the second level of the arithmetical hierarchy independent of PA?

If I am not wrong, every $\Sigma_n$ (or $\Pi_n$ ) statement $\phi$ is equivalent to a statement that says that a given Turing machine halts (or doesn't halt) on input $C$ using a ...
3
votes
1answer
109 views

Can decidability results for monadic second-order logic be extended to monadic higher-order logics?

Call a higher-order logic fully monadic if and only if all of its predicate constants (at any order) and higher-order variables (at any order) are monadic (and it has no function symbols). In Solvable ...
5
votes
3answers
261 views

How are the full semantics of SOL and HOL specified?

In relation to this question about the "fundamental" character of possible logical systems, I realized that I just had an intuitive (and so, inadequate) understanding of the way logics higher than FOL ...
12
votes
1answer
506 views

Is First Order Logic (FOL) the only fundamental logic?

I'm far from being an expert in the field of mathematical logic, but I've been reading about the academic work invested in the foundations of mathematics, both in a historical and objetive sense; and ...
8
votes
1answer
417 views

Second-order logic - monadic version and Henkin semantics

After looking at texts and Wikipedia, I am getting some confusion on difference between monadic second-order logic and full second-order logic and difference between Henkin semantic and full semantic. ...
4
votes
1answer
423 views

advantage of first-order logic over second-order logic

As I look over the post that has the similar question, I began to wonder: The only reason I found is that first-order logic can prove validity of some second-order logic formula/sentences, as some of ...
3
votes
2answers
235 views

What makes higher/second-order logic incompatible with completeness theorem?

Completeness theorem and compactness theorem do not hold in full second and higher-order logic. What makes them incompatible with the theorems? Is it somehow related to Russell's paradox or ...
6
votes
1answer
368 views

First-order logic advantage over second-order logic

What is the advantage of using first-order logic over second-order logic? Second-order logic is more expressive and there is also a way to overcome Russell's paradox... So what makes first-order ...
3
votes
1answer
94 views

Formal second-order statements of Archimedean and completeness properties

I am trying to translate the following statements from English to second-order logic, and I want to know if I got them right. I have a language for an ordered field $(F,+,\cdot,0,1,\leq)$, i.e., I ...
2
votes
1answer
225 views

Independence results in first-order PA and second-order PA

There are statements $\varphi$ that are independent of first-order Peano Axioms. Are these statements also independent of second-order Peano Axioms? I'm reading Wikipedia articles around ...
2
votes
2answers
159 views

Are $\{X \in 2^{A}:|X|=2\}$, $\{X \subset 2^{A}:|X|=2\}$, $\{X \subset A:|X|=2\}$ first order or second order?

Are those statements first order or second order: $$\{X\in 2^{A}:|X|=2\} \\ \{X \subset 2^{A}:|X|=2\} \\ \{X \subset A:|X|=2\}$$ why?
2
votes
0answers
79 views

Introductory text about different stratification methods in higher-order logic and set theory

Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
1
vote
0answers
71 views

Differential fields and rings

If one is to compute the derivative of $$ y=3x+2 $$ by $$ \frac{\mathrm{d}(3x+2)}{\mathrm{d} x} $$ Would I be working with differential fields? Since differential fields is a first-order ...
3
votes
0answers
155 views

Is there such a thing as “second-order-undecidability”? And what about higher order Undecidability statements?

I know that there are statements that are neither provable nor disprovable within some set of axioms, and I also know that such statements are called undecidable. Please allow me to call these ...
4
votes
0answers
265 views

logic lectures on youtube

Currently I am reading Logic an Structure by Dirk van Dalen (2008). As I am missing some basics I try to find related lectures on youtube. I frequently watch MIT, Stanford, and University of ...
5
votes
3answers
319 views

Higher Order Logics

I've read about about higher-order logics (i.e. those that build on first-order predicate logic) but am not too clear on their applications. While they are capable of expressing a greater range of ...