# 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
Filter by
Sorted by
Tagged with
1 vote
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
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
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
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
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
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?
1 vote
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
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 vote
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. ...
66 views

• 3,921
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
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
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
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
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
49 views

• 1,041
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
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
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 ...
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
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
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
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
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
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 (...
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
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 ...
88 views

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 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
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 ...