Questions tagged [first-order-logic]
For questions about formal deduction of first-order logic formula or metamathematical properties of first-order logic.
5,071
questions
1
vote
0
answers
15
views
The validity of $∀x(Bx↔∃yRxy)↔\big(∀x∃y(Bx→ Rxy)∧ ∀x∀y(Rxy→Bx)\big)$
$(\forall x.B(x) \leftrightarrow \exists y. R(xy)) \leftrightarrow (\forall x \exists y.B(x)\rightarrow R(xy)) \land \forall xy. (R(x,y) \rightarrow B(x))$ is a valid formula.
My attempt to prove the ...
- 1,737
0
votes
0
answers
79
views
Are these axioms sufficient as a logical foundation for ZFC?
My question is: are the following axioms sufficient as a logical foundation for ZFC? I just want to be sure that I'm not missing any axiom.
I took them from the first chapter of the book "...
- 743
1
vote
0
answers
12
views
Decidability of discrete variable predicate calculus
Question.
Is a predicate logic with discrete variables decidable? If yes, than whats is algorithm to obtain statement about truthiness of particular sentence?
If yes, it would be good to have ...
- 321
6
votes
1
answer
252
views
What is the justfication for splitting up statements and quantifiers?
To explain the title, in proving $X \times Y = \emptyset \iff X = \emptyset \vee Y = \emptyset$, we have the following
\begin{align*}
X \times Y = \emptyset &\iff \forall x \forall y \left((x,y) \...
- 520
0
votes
0
answers
34
views
Is non-Noetherianness first order axiomatizable in the language of commutative unital rings? [duplicate]
By a standard argument* using Łoś's ultraproduct theorem (either directly or through the compactness theorem), Noetherianness is not first order axiomatizable in the language of commutative unital ...
- 974
0
votes
0
answers
19
views
Are functions required to be total in first-order logic? [duplicate]
Are functions usually required to be total in the context of first-order model theory?
If so, how can one deal with partial functions?
- 173
1
vote
0
answers
24
views
Free variables in derivation systems
I work relative to a fixed first-order language $L$. As usual I call those formulas which do not contain free variables sentences. There are several derivation systems for first-order logic. For ...
- 3,206
-1
votes
0
answers
8
views
Subsumption in Polynomial-Time for EL Description Logic extended with non-Nested Negations
Is the subsumption between two formulas of the EL Description Logic extended with non-Nested Negations decidable in polynomial time ?
EL extended with non-Nested Negations is defined by :
Concept ...
- 1
1
vote
1
answer
50
views
Are there Nonstandard Models of Arithmetic that don't Add Additional Axioms?
Apologies if this is an elementary question that should have been obvious to me. I am learning about these topics very much from the perspective of an outside hobbyist, and am not a wizard of logic.
...
- 11
0
votes
1
answer
66
views
Logic - Is it possbile that two formulas represent the same set in some theory T, but they are not equivalent?
I am working on exercises from logic lectures. Here's one question which confuses me:
Suppose that a formula $\varphi(x)$ represents the set $A$ in $T$, where $T$ is a true theory. Also suppose that $...
- 3
2
votes
0
answers
32
views
How can I prove that $\vdash \exists \overline{z}(\overline{z}=\{x,y\})$
I'm studying the one-sorted version of NBG (Neumann-Bernays-Gödel) Class Theory (that is, NBG with only one alphabet). I want to prove that $\vdash \exists z(\exists Z(z\in Z)\wedge z=\{x,y\})$ but I ...
- 743
2
votes
1
answer
91
views
Why use LF to define type theories?
I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers LF, ...
- 223
-1
votes
0
answers
33
views
Existential elimination rule in natural deduction
This is the rule of Existential Elimination: ∃xAx ⊢ B
Can Ac be inferred directly from ∃xAx, given c is assumed to have the property A?
For qS-tree proofs, it is a valid rule to infer Ac from ∃xAx and ...
- 21
2
votes
1
answer
39
views
Counterexample to most general unifier example
I am reading these slides about unifiers and most general unifiers (MGUs): https://artint.info/2e/slides/ch13/lect3.pdf
In particular, an MGU is defined as follows. A substitution $\sigma$ is an MGU ...
-3
votes
1
answer
142
views
order property vs. antisymmetric property
The definition of order property is well known:for a first-order theory $T$ the order property means that for some first-order formula $\phi(\bar{x},\bar{y})$ linearly orders in $M$ some infinite $\...
- 3,921
0
votes
1
answer
41
views
Every subset of $\Bbb N$ is defineable in the language of monoids
Let $\mathcal L=\{\cdot,e\}$ be the language of monoids so that $\cdot$ represents an operation which is closed and associative, and $e$ represents an identity. Consider the structure of natural ...
- 4,969
1
vote
1
answer
61
views
In First Order Logic, why are we allowed infinitely long sets of finite formulas, but not infinite formulas?
Consider the empty language $L = \{\}$. Then we are said to be able to define the set of infinitely many elements, say $K = \{x_1,\cdots,x_n,\cdots\}$, as the set satisfying the infinite set of finite ...
- 135
4
votes
1
answer
116
views
Reasoning in natural language vs. reasoning in formal language
In ZFC set theory, we first used axioms to prove the existence of the set of natural numbers based on its definition, and after proving uniqueness, we introduced $\mathbb{N}$ in a new symbolic system ...
- 1,748
1
vote
1
answer
64
views
Is there a G4ip equivalent for first-order logic?
G4ip is a sequent calculus for propositional logic (by Dyckhoff) that is contraction-free, thus (if I understand correctly) greatly simplifying the writing of automated theorem provers by avoiding ...
- 13
0
votes
1
answer
57
views
Forcing $\pi_1(\tilde f(a))=f(a)$ for an object of a sigma type
Suppose I have an object $f$ of type $\Pi x:A.B(x)$, and consider a new type $\Pi (x:A).\Sigma (t:B(x)).C(t)$. If $\tilde f$ is an object of the second type and $a:A$, then $\pi_1(\tilde f (a)):B(x)$, ...
- 223
0
votes
0
answers
49
views
Proof in Natural Deduction, Sequent Calculus or Hilbert System
Is there any smart way to check if certain statements are not provable in any of these proof systems?
Like for example the following task:
Prove or disprove the following statements:
$\vDash \exists ...
- 69
0
votes
2
answers
65
views
Adding $\tfrac{}{\Gamma \varphi}$ (for a fixed non-correct $\Gamma \varphi$) to the rules of the sequent calculus, can one now derive every sequent?
One knows that the sequent calculus over the set of sequents $\Gamma \varphi$ is correct and complete, meaning that the derivable sequents are precisely the correct ones.
However, adding just one ...
- 33
0
votes
1
answer
74
views
Question on finite structures
I need to find a sentence such that it is valid for all finite structures but false in some infite structure. I've couldn't find any sentence that includes only "=" to be true in finite ...
- 83
2
votes
1
answer
62
views
Definition of first order logic and property.
$\newcommand{L}{\mathcal{L}} \newcommand{A}{\mathcal{A}} \newcommand{Trm}{\operatorname{Trm}} \newcommand{Frm}{\operatorname{Frm}}$
I am reading the first order logic (FOL) section in the Open Logic ...
- 113
0
votes
0
answers
61
views
Is there any link between Turing machines and proof theory?
I was told (in an informal way) that there exists a close link between Turing machines (or recursive functions, which amounts to the same) and proof theory in the sense that any formal proof can be &...
- 169
5
votes
1
answer
259
views
Is there a technical reason to require relation symbols to have positive arity?
I've noticed that many logic textbooks (oriented towards model theory) will require relation symbols to have positive arity. I cannot immediately think of a technical reason why one would require this ...
- 331
0
votes
1
answer
31
views
How do I show if (∀x∃y∀zP(x, y, z)) ⇒ (∃y∀x∀zP(x, y, z)) is a logically valid statement?
I have tried to add a double negation to the left hand side and then swap the existential quantifiers, which gives:
¬¬∀x ∃y ∀z P(x, y, z) ⇔
¬∃x ¬∃y ∀z P(x, y, z)
This, I thought, means I can swap the ...
- 11
2
votes
2
answers
75
views
Some first order sentences for free groups.
I'm looking for some examples of sentences in the elementary theory of free groups. For example, let $F$ be the free group on 3 generators, how can I capture the idea of freeness in a first order ...
- 21
1
vote
0
answers
30
views
Syntax variants for functions and predicates in first-order logic
There seem to be at least three syntactic conventions in common use for function terms and predicate formulas in first-order languages. Specifically (where $\mathfrak{F}$ is an arbitrary function or ...
- 169
1
vote
0
answers
49
views
Soundness and completeness of Fitch-style for first order logic
I am looking for literature in which a detailled proof of the soundness and completeness of Fitch-style proofs for first order logic is given. In his 1952 book "Symbolic Logic, An Introduction&...
- 171
0
votes
1
answer
28
views
How to perform induction on the number of connectives and quantifiers in a well-formed formula?
I am trying to prove the following proposition from Mendelson's book.
If the free variables (if any) of a well-formed formula $\textbf{B}$
occur in the list $x_{i_1}, \dots, x_{i_k}$ and if the ...
- 1,041
4
votes
1
answer
108
views
Proof that the order of quantifiers doesn't matter (what went wrong)?
I believe the order of quantifiers in a sentence matters, but I made this proof that basically says it doesn't, what am I doing wrong?
PROOF
$$\forall x\exists y(\phi(x,y))$$
$$\iff$$
$$\exists y\...
8
votes
2
answers
216
views
Is 1+1=2 logically equivalent to 99+1=100?
I am trying to understand logical equivalence.
From what I understand, two formulae are logically equivalent if they have the same truth values under all interpretations. So,
$$x+1=y\dashv\vdash x+(2-...
0
votes
1
answer
45
views
How to prove uniqueness with uniqueness quantification? (Uniqueness of the Axiom of Specification)
I really like the uniqueness quantifier $\exists!$, but I don't know how to prove formulae with it.
I am trying to prove:
$$\forall X\exists!Y\forall x(x\in Y\iff x\in X\land\phi(x))$$
from the ZFC ...
0
votes
2
answers
58
views
How to understand one of the properties of satisfaction of wfs in first-order logic?
Proposition:
If the free variables (if any) of a well-formed formula $\textbf{B}$
occur in the list $x_{i_1}, \dots, x_{i_k}$ and if the sequences $s$
and $s^′$ have the same components in the ${i_{1}...
- 1,041
0
votes
0
answers
39
views
Tarski-Vaught Test with languages without constants
Does the Tarski-Vaught Test apply to structures of languages that do not contain any constants? From the proofs I've tried to find in textbooks, it relies on quantifier elimination which also relies ...
- 779
-3
votes
1
answer
63
views
Infinite axioms/Group of axioms
When we talk about an axiom, shouldn't it be a group of axioms since we have an axiom for each variable?.
For example, "B ⇒ (C ⇒B)" is an axiom schema standing for an infinite number of ...
- 9
0
votes
0
answers
25
views
How can I show that if a theory T is closed under extension, then it can be axiomatised using existential sentences? [duplicate]
If M and N are two models and the inclusion M ⊆ N is an embedding,then N is an extension of M.
An existential sentence is a sentence which consists of a string of existential quantifiers followed by a ...
- 1
0
votes
0
answers
102
views
Value of the function. (First order set theory foundations ZFC. Interpretation with partial functions.)
I am convinced that the following is true, I just need to double check myself, and also maybe share this with a community, since I find it beautiful.(if it is true)
Let us consider "the standard ...
- 760
0
votes
0
answers
89
views
How is "choose" used here formally?
It happens a lot that there is some set $X$ and choosing some objects such as elements of some set or functions (...) one constructs a new object using this choice. More precisely, suppose $X$ is a ...
- 157
0
votes
1
answer
69
views
Is every function a relation in first-order logic?
When dealing with functions outside of formal languages, the concept of 'function' and of 'binary relation' are such that the set of all functions is a subset of binary relations.
For example using ...
- 167
4
votes
0
answers
129
views
Confusion about Gödel's Completeness Theorem
I am interested in the following question just because it feels as if I am not able to figured it out on my own. It seems there is some mistake in my thinking.
Let $T$ be a theory in some first-order ...
- 1,627
1
vote
1
answer
75
views
How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)? A method of natural deduction.
Logic is something I am entirely self-taught in. Due to my resulting ignorance, it is difficult for me to search for the right things. Therefore, please excuse me if this has been asked before.
The ...
- 41.8k
0
votes
1
answer
77
views
Circularity on Unique Readability for Terms [closed]
I have begun self-studying Logic (I am a numerical physicist), and I am stuck at the very beginning. I have a problem with the proof of the Unique Readability Theorem for Terms in First Order Logic (...
- 1
19
votes
8
answers
3k
views
Don't Understand Mechanism behind Proof by Contradiction
I believe there are two kinds of proof by contradictions, one which I understand, and another one which I have some questions. I'll begin with the first one.
1st CASE
Suppose I can logically show that ...
- 207
-2
votes
1
answer
84
views
Theorems in FOL and Propositional Logic [closed]
In some computer science articles, they define a theory (with axioms) then write a series of theorems based on the theory. In propositional logic, it seems that a theorem is what follows from natural ...
- 19
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)...
- 692
0
votes
1
answer
91
views
How to derive $ \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z))$?
I have to give a natural deduction proof of the statement:
$$ \emptyset \;\; \vdash \;\; \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z)) $$
This is a valid formula as per ...
- 2,005
0
votes
2
answers
61
views
Can every first-order theory be conservatively "second-order-ized"?
Basically the idea is to define comprehension over first-order formulas in $T$. I give complete details below, but as a preview
Questions:
Starting from an arbitrary (single-sorted $O$) first-order ...
- 1,134
0
votes
0
answers
49
views
which notion of provability in Turing's paper 1936?
In Turing's article 1936 https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
Turing provides a proof in §11 p.259 for the Hilbert decision problem "Entscheidungsproblem".
p. 259 he ...
- 169