The tag has no wiki summary.

learn more… | top users | synonyms

3
votes
1answer
35 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 ...
1
vote
0answers
46 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
34 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 ...
0
votes
0answers
19 views

Least finite linear orders with same theory in monadic second order logic.

Today I want to ask a relaxed version of my last question. So if somebody finds a solution to that question he will immediately get a solution for this question here. Question. Let $m<\omega$ ...
2
votes
0answers
28 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
69 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
58 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
29 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
358 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
67 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
132 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
55 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 ...
0
votes
0answers
24 views

higher order schemes or curvature to be smoothed

I want to calculate the radius of curvature of a meandering river. I have done a first estimated using a tool in arcgis. These are the results. The values of -99999 are recorded for points of no ...
2
votes
1answer
54 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
75 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
55 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 ...
2
votes
2answers
209 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
37 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
30 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
49 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. ...
0
votes
0answers
13 views

Simplest manual or set of examples on (monadic) second-order logic

It is needed simplest manual where second-order logic, especially its monadic restriction, will be explained step-by-step on several examples. It is also needed to explain syntax of SOL formulae in ...
2
votes
0answers
84 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
863 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
117 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
43 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
76 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
63 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
106 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
65 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
90 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
100 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
124 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 ...
5
votes
4answers
226 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
74 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 ...
2
votes
2answers
99 views

annihilator method confusion

I have a final in the morning and I am extremely confused on the annihilator method. I have been googling different explanations all night and I just dont get it at all. I am looking at an example: ...
2
votes
1answer
82 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 \; ...
7
votes
2answers
177 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
42 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 ...
4
votes
1answer
162 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
123 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
185 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
94 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
54 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. ...
3
votes
1answer
150 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
59 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
85 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
147 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
225 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
218 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
1k 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 ...