Questions tagged [second-order-logic]
The second-order-logic tag has no usage guidance.
173
questions
2
votes
0
answers
88
views
A Question regarding Properties of predicates and the definition of the Quantifiers
Here are some properties of predicates that I found.
$$1.\;¬(∀x)ϕ(x) ⇐⇒ (∃x)¬ϕ(x)$$
$$2.\; (∀x)(ϕ(x) ∧ ψ(x)) ⇐⇒ ((∀x)ϕ(x) ∧ (∀x)ψ(x))$$
$$3.\; (∃x)(ϕ(x) ∨ ψ(x)) ⇐⇒ ((∃x)ϕ(x) ∨ (∃x)ψ(x))$$
$$4.\; ((∀x)...
0
votes
0
answers
31
views
Completeness Axiom of L2Real is True under an interpretation about probability in GTM53
In Chap 3 of GTM53, there is an interpretation of L2Real where the symbols of numbers is interpreted as a random variable. I cannot finish the proof of the completeness axiom of reals $\forall f(\...
0
votes
2
answers
42
views
What is the best way to define a generically finite set?
I'm trying to write a proof to show that a tree structure of finite nodes terminate.
Suppose we can say that either a node is a parent of another node ($Pqp$: $q$ is the parent of $p$), or it is a ...
4
votes
1
answer
114
views
Can we axiomatize the complex numbers without directly defining the reals?
I've decided to attempt the entire Rudin sequence in a single 6 month period, because I'm insane. Rudin spends very little time on foundational matters, and that bothers me, it makes the subject of ...
1
vote
0
answers
36
views
Does Tarskian semantics use a "larger set theory" to implement second order logic?
My background knowledge:
My (poor) understanding of Tarskian semantics is that we are given both:
a theory/formal language of first-order logic to be used as the object theory, and
a "larger&...
1
vote
1
answer
61
views
Non-Henkin non-full semantics for second-order logic
I'm interested in alternative semantics for second-order logic that still have a first-order flavor the way that Henkin semantics does.
Let's consider a version of second-order logic with a single ...
0
votes
2
answers
70
views
Formalizing the notion of a finite number of steps.
Suppose we have a (potentially infinite) graph $G$. Let $xRy$ denote the statement "there exists a directed edge from $x$ to $y$" for some two nodes $x, y$ of $G$. I'm interested in a ...
1
vote
1
answer
61
views
What recursive extensions are there of axiomatic second-order logic.
There are two semantics used for second-order logic, Henkin semantics and standard semantics. It’s easy to make a recursive deductive system $D$ that is sound and complete with respect to Henkin ...
0
votes
0
answers
25
views
Why can't IF have a Tarskian semantics? Does the following semantics for an IF-like system fail to be Tarskian?
I'm thinking about independence-friendly logic because I saw meta-level use of "independent of" in the definition of elimination of imaginaries in Hodges' A shorter model theory.
That got me ...
1
vote
2
answers
113
views
Is the theory for $\mathbb{R}$ categorical or not?
The usual axioms of $\mathbb{R}$ consist of the ordered field axioms plus the least upperbound property. Because the least upperbound property is a statement that quantifies over sets of real numbers, ...
1
vote
1
answer
49
views
Quantifying Over Functions In Henkin Semantics
I am trying to understand the Henkin Semantics for Second Order logic and, and I’m confused on the following point.
The Comprehension Axioms are typically defined as follows: for every second order ...
1
vote
1
answer
74
views
Why is does this first-order set of axioms NOT genetically define the natural numbers?
It is a theorem of model theory that any recursively enumerable set of axioms $\Gamma$ for number theory permit non-standard models. That is, if there is one model for $\Gamma$, then there are two ...
1
vote
0
answers
28
views
Has it been proven that second order statements cannot be computed in polynomial time? Can some statements be proven to only be second order expresibl
I have read about the Immerman Vardi theorem and I do not understand what the implications fully are. Does it say that second order logic cannot be expressible in polynomial time? Or merely that all ...
3
votes
1
answer
116
views
Continuous First order logic vs Second order logic
By continuous first order logic I mean first order logic but replace truth values taking on 0 or 1 with the compact set [0,1].
Is continuous first order logic strong enough to make statements about ...
2
votes
0
answers
46
views
EER model or relational model for second order logic statements
Question.
I know that EER model and relational model (database schemas where tables are connected with arrows) can be used to express first order predicate logic statements for case when variables are ...
0
votes
0
answers
28
views
Reverse mathematics and Peano categoricity, a question
Simpson and Yokoyama in the paper
"Reverse mathematics and Peano categoricity"
Try to show that in RCA0, if weak konig lemma doesn't hold, then Peano categoricity doesn't hold either. This ...
0
votes
0
answers
20
views
A fast growing functions in $\sf{ACA_0}$ and $\sf{Z_2}$
There is a fast growing function whose totality is not provable in a subsystem of second order arithmetic called $\sf{ACA_0}$: the Paris-Harrington function. I would like to know the name (and the ...
2
votes
0
answers
42
views
Is the positive fragment of second-order logic will full semantics compact?
There are two slightly different versions of compactness:
If $\Delta$ is finitely satisfiable, then $\Delta$ is satisfiable.
If $\Gamma \models \varphi$ then there exists a finite subset $\Gamma_0 \...
0
votes
0
answers
21
views
subsytems of second order arithmetic
Consider the 5 prominent subsystems of second order arithmetic.
I would like to know which of these subsystems of second order arithmetic have computably axiomatizable theory.
2
votes
0
answers
51
views
A Peano system with an infinite initial segment
Let $T$ be a binary tree with the lexicographic order. And $f:T→T$ be the successor operation.
We denote the empty sequence in $T$ by $i$.
Also Suppose that:
For all $X⊂T$ if these two conditions hold:...
0
votes
0
answers
36
views
The set of all finite sequences in RCA0
In the book "subsystems of second order arithmetic", page 68, Simpson claimed that the set of all codes of finite sequences (denoted by "Seq") exists by sigma 0-0 comprehension. I ...
0
votes
0
answers
28
views
Primitive recursion in $RCA_0$
In $RCA_0$, let $T$ be a binary tree. Define $P : \mathbb{N} \to \{0,1\}$ by this:
$$P(n) = \begin{cases} 1 & \langle P(0), P(1), \ldots, p(n-1), 1 \rangle \in T \\ 0 & \text{otherwise} \end{...
3
votes
0
answers
31
views
In RCA0, Prove that for all n, fⁿ(i) exists
I wanted to prove in RCA0 that:
If f:A→A be a function and i∈A, then for all n, fⁿ(i) exists.
To reach that, I proved another theorem. I wrote my proof but I'm not sure it's rigorous. If you read it, ...
0
votes
1
answer
51
views
Does Z₂ Prove the iteration theorem?
iteration theorem:
Let (ℕ,0,S) be the structure of natural numbers. And let W be an arbitrary set and c be an arbitrary member of W and g be a function from W into W. Then, there is a unique function ...
1
vote
0
answers
40
views
What is the importance of Peano categoricity?
We know that Dedekind in 1888 proved that second order peano arithmetic(PA2) is categorical. My question is, why is it important? Does it have any mathematical, philosophical or foundamental ...
1
vote
0
answers
29
views
Peano categoricity is equivalent to weak konig lemma
Peano categoricity (PC) says that:
Every model for second order peano system is isomorphic to standard model.
i.e PC says that every peano system such as
(A, f, i) is isomorphic to (N, S, 0).
Simpson ...
0
votes
0
answers
53
views
Is there such a thing as the second-order theory of a structure?
Given a structure, say for example, $(\mathbb{R};+,*,0,1,<)$, I know the definition of the first-order theory of that structure. But is there such a thing as the second-order theory of a structure, ...
1
vote
0
answers
57
views
Are there expressive compact fragments of universal second order logic?
Question 1: I'm interested in fragments of universal second-order logic (USO) that are known to be compact. Are there any that, for example, include negation or first-order existential quantification?
...
0
votes
0
answers
42
views
How can higher-order logic be expressed as many-sorted first order logic?
I know that second order logic (or higher order logic generally speaking) can be expressed using many-sorted first order logic. But I am unclear about the specifics.
Say I have predicate variable $\...
1
vote
0
answers
23
views
Hypotheses of the quadratic convergence of a real serie $x_k$
My book claims that a serie has a quadractic convergence if $\forall x_k$, $k = 1, 2, \dots$:
\begin{equation}
|x-x_{k+1}| \le C|x-x_k|^p
\end{equation}
such as $C \in \mathbb{R}$ and $p = \color{...
1
vote
0
answers
72
views
Proofs that monadic second order logic is not compact
I was reading this comment by Simone on this answer to this question.
The comment is reproduced below, emphasis mine.
Well, It's not an extension that uses the notation you use, but all axioms remain ...
5
votes
1
answer
259
views
Why is ZFC incapable of interpreting second-order logic?
Why is ZFC incapable of interpreting second-order logic?
Also, when we say this, are we talking about ZFC as a background theory or using ZFC in some different way?
I am interested in this answer ...
0
votes
0
answers
50
views
Questions about smt-solvers.
Are smt-solvers (like z3) theoretically able to (always correctly) check consistency of any 1.-order logic formula?
How does smt-solver algorithm work in details?
Are there any algorithms that could ...
2
votes
0
answers
25
views
Strength and conservativity of $\Sigma^1_n \textrm{-DC}_0$
How strong is $\Sigma^1_n \textrm{-DC}_0$ in terms of consistency strength? I know it is conservative to $\Pi^1_n \textrm{-TI}_0$, but I don't know its relation to other subsystems. Are there any ...
0
votes
0
answers
40
views
Logic with predicate symbol of arbitrary arity
For the work I am doing on abduction inference, I need a second order many-sorted logic where the only predicate symbol $\psi$ of the first order formulas may have an arbitrary arity. I may assume ...
0
votes
0
answers
78
views
Prove the Archimedean property from second-order Dedekind completeness OR prove the existence of the integers.
Context:
I am taking an introductory real analysis class (because I need the credit), and the professor has provided me with their notes on the subject. In the notes, the professor defines the real ...
0
votes
0
answers
39
views
Second-order arithmetic subsystems
I've been surfing the internet, and have found some subsystems or additional axioms of second-order arithmetic whose definitions I could not find. Does anyone know what the following axioms/subsystems ...
-1
votes
1
answer
86
views
Proving $\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$
I'm trying to prove the following:
$$\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$$
The following is my first attempt. However, I'm not sure if I can just drop ...
0
votes
0
answers
69
views
Is there a "canonical" form of second order logic?
For the sake of comparison, the entirety of first-order logic can be summarized as follows:
The well formed formulas of first order logic are those generate by the grammar:
$$\begin{align}
&\...
6
votes
0
answers
104
views
How big a "scaffold" does second-order logic need to detect its own equivalence notion?
(Now asked at MO.)
Let $\Sigma$ be the language consisting of a single binary relation symbol. Second-order logic can "detect" second-order-elementary-equivalence of $\Sigma$-structures in ...
0
votes
1
answer
118
views
Validity of theorems using natural numbers and irrational reals together
I read in other posts (like in this answer) that the natural numbers are not definable in the first-order theory of the real numbers- That is considering just the reals within the context of a real ...
0
votes
1
answer
47
views
Satisfiability of Second-Order Logic: Is this Decision Problem Complete for Some Level of the Arithmetical Hierarchy?
Consider the following decision problem defined in terms of input/output:
Input: a second order logic [1] theory $\mathcal{T}$ (i.e., $\mathcal{T}$ is a set of second order logic formulas)
Output: ...
1
vote
3
answers
117
views
Is there a model of $\operatorname{Th}(\mathbb{R})$ which is not a complete ordered field?
As far as I understand completeness (every non-empty subset bounded from above has a supremum) is a second order property. Is there a model of $\operatorname{Th}(\mathbb{R})$, the first order theory ...
0
votes
1
answer
66
views
Can second order ZFC have a set model
Second order ZFC cannot have a countable model.
Can it have a set model (in full semantics) of size $\kappa$ for some cardinal ? What can be said about such a $\kappa$ ?
1
vote
0
answers
93
views
Definition of ZFC2 (second order logic)
ZFC with 1st order logic is known.
My question may be formulated either way
What is the definition of ZFC2 (ZFC+second order logic)? (I assume that formulas also have quantifications of two kind over ...
9
votes
1
answer
161
views
Does the absolute fragment of second-order logic satisfy a strong Lowenheim-Skolem property?
Let $\mathsf{SOL_{abs}}$ be the "forcing-absolute" fragment of second-order logic - that is, the set of second-order formulas $\varphi$ such that for every (set) forcing $\mathbb{P}$ and ...
0
votes
1
answer
33
views
Which to use for this relational calculus query, the "for all" quantifier" or the "there exists" quantifier?
Let's say the following relations are given:
Sailors(sid, sname, rating, age)
Boats(bid, bname, color)
Reserves(sid, bid, day)
What will be the tuple relation calculus query to Find the sailor name, ...
0
votes
1
answer
183
views
When to use the "there exists" quantifier in tuple relational calculus?
Let's say we're given the following relation: Sailors(sid, sname, rating)
And we have to answer the following query: The names of all sailors with a rating above 7.
What will be the tuple relational ...
-2
votes
1
answer
116
views
Is there a class of finite graphs that can be axiomatized by existential second-order formulas but it's complement couldn't? (edited) [closed]
I'm interested in the question above. I've just the add the "finite" requirement.
1
vote
1
answer
98
views
What is the interpretation of Presburger Arithmetic in WS1S?
It’s my understanding that Julius Büchi showed that $WS1S$, the weak monadic second-order theory of one successor is decidable by a finite-state automaton, and that this implies that Presburger ...