Questions tagged [first-order-logic]

For questions about formal deduction of first-order logic formula or metamathematical properties of first-order logic.

2,903 questions
36 views

Definition of Semantic Entailment in First-order Theory

I cannot understand the meaning of the soundness theory in first order logic. It says that if $S$ syntactically entails $p$, then $S$ semantically entails $p$. However, $p$ don't have to be a ...
44 views

Exercises involving Morley rank & degree

The definitions of Morley rank & degree I use are I understand these definitions, but I am having a hard time to use them concretely in exercises. For example, Let $L$ be a countable language ...
35 views

Logical programming

“Anyone who eats junk food or drink carbonated beverages will be a cancer victim. It is not the case that some people eat junk food but they are healthy. Every cancer victims are not healthy. Bimal is ...
41 views

43 views

Truth value of an open formula

I've always thought that an open formula, i.e. a formula containing free variables, has no truth value. For example, strictly speaking, I would say that for $x\in\mathbb R$, the formula "$x^2\geq0$" ...
15 views

Can full Replacement be proved from replacement from sets of ordinals?

In a prior posting about "Ordinal Replacement", Joel David Hamkins had answered it, and his answer included the following statement: In fact, in this case, we needn't restrict $B$ to consist of ...
62 views

16 views

FOL-Interpretation of a tableaux

Suppose I have the FOL-Formula $F := \forall x \exists y. R(x, y)$ in negation normal form. Now I want to show that $F$ is satisfiable using the tableaux calculus (TC1). By application of rules I get ...
56 views

MGU - most general unifier for skolem functions?

I have trouble understanding MGU for functions, especially skolem functions. Is it correct that in order to find MGU for 2 functions, say f(x) and g(y) then they ...
68 views

Ideal treatment of set theory as a meta theory for developing first-order logic

I am very familiar with the fact that when introducing model theory and the meta theorems describing a formal system, set theoretic notions are inevitably required which we include in the meta theory. ...
24 views

Prove that $\Gamma$ $\vdash$ $\phi$ iff. $\Gamma$ $\vdash$ $\phi_c^x$ for any constant symbol c not occuring in $\Gamma$

i have a bit problems with this, $\Gamma$ is a set of sentences in a language, and let φ be a formula in the language. can anybody help, im pretty lost
66 views

Proof that Peano Axioms is a theory with equality (according to Mendelson book)

I'm reading Elliott Mendelson's "Introduction to Mathematical Logic". There is a statement with a proof that $S$ (Peano Arithmetic) is a first-order theory with equality. I am not sure whether I ...
26 views

Can this simplified arithmetical theory with a syntactically non reachable last natural be complete?

The following theory is coined in the language of arithmetic, however it differs in that the successor, addition and multiplication functions are not total functions. Also we add a new constant $L$ to ...
81 views

Statements vs Formulas

In A Tour Through Mathematical Logic, Wolf states that Every formula of a first-order language is a statement in the sense of Section 1.2, but not conversely. In Section 1.2, Propositional Logic,...
36 views

How to write an implication whose antecedent quantifies a variable in its consequent?

I want to write the statement $$\text{If } A^{-1} \text{ exists then } A^{-1} = \frac{\alpha-a}{\alpha^2-a^2}$$ using quantifiers. Note that $A$ and its inverse, if it exists, are taken from the set ...
81 views

Derivative proof involving MVT and Rolle's Theorem

Suppose $f$ is a continuous and differentiable function on $[0,1]$ and $f(0) =f(1)$. Let $α∈(0,1)$. And $$∀x,y∈(0,1) ,f′(x)\neq 0\wedge f′(y)\neq 0\rightarrow f′(x) \neqαf′(y)$$ Show ...
24 views

On rewriting the statement into predicate logic.

I'm interested in rewriting mathematical statement into predicate logic. Is the following correct? Normal Expression the following $x$ exists, such that $x \in R,x^2-1=0$ Predicate Logic ...
63 views

Deduction for $\exists v_1 \forall v_2 \lnot f(v_2) = v_1 \vdash \exists v_1 \exists v_2 \lnot v_2 =v_1$

I'm trying to find a deduction for $$\exists v_1 \forall v_2 \lnot f(v_2) = v_1 \vdash \exists v_1 \exists v_2 \lnot v_2 =v_1$$ with these axioms & lemma. For any function $f$ and relation $R$ ...
54 views

Logical Axioms and Rules of Inference

In A Tour Through Mathematical Logic, Wolf mentions that These [logical axioms] usually include some or all tautologies, the usual equality axioms, and some simple laws involving quantifiers. ...
82 views

Resolution Principle in First Order Logic

Suppose that we are in First Order Logic and we have a set of clauses. I want to prove that a certain clause is a logical consequence of this set of clauses. Is it correct to use the Resolution ...
31 views

Can this simple form of double extension set theory escape inconsistency?

The following theory is another way of dealing with naive comprehension. It uses the double extension principle, broadly speaking similar to what's used in Double Extension Set Theory of Andrzej ...
55 views

Is this theory of arithmetic with a last natural that is not reachable from below complete?

This theory is a theory of arithmetic having a last natural number that is not reachable from below by syntactical recursive iteration of the successor function. So it doesn't prove all rules of ...
47 views

Natural Deduction: Universal Introduction rule concerning free variables in Van Dalen's “Logic and Structure”

The $\forall I$ rule (forall introduction) in Dirk van Dalen's Logic and Structure (4th ed) is: $${\forall I}\, \frac{\varphi}{\forall x\, \varphi}$$ where the intended restriction is: the variable ...
47 views

every relation in a special structure $M$ which is first-order definable with parameters has cardinality $< \omega$ or $= |M|$.

Let $M$ be a special structure. I'm trying to proof that every relation in $M$ which is first-order definable with parameters has cardinality $< \omega$ or $= \lambda$. By a first-order definable ...