Questions tagged [second-order-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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(\...
  • 61
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 ...
  • 4,440
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 ...
  • 9,228
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 ...
  • 365
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 ...
  • 9,228
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,043
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 ...
  • 33
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 ...
  • 311
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 ...
  • 3,901
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 \...
  • 9,228
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.
  • 3,901
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, ...
  • 16.8k
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? ...
  • 9,228
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 ...
  • 9,228
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 ...
  • 9,228
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 ...
  • 263
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 ...
  • 193
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 ...
  • 4,440
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 ...
  • 263
-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 ...
  • 1
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} &\...
  • 4,440
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 ...
  • 679
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 ...
  • 85
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$ ?
  • 3,901
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 ...
  • 760
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, ...
  • 328
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 ...
  • 328
-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 ...