Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange
Join us in building a kind, collaborative learning community via our updated Code of Conduct.

Questions tagged [first-order-logic]

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

2
votes
3answers
46 views

Equivalence in natural deduction in First-order logic

Task $\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $ My answer If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$. So I started trying to see if I could prove $B$ ...
2
votes
1answer
40 views

Natural deduction in first-order logic

I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below. $\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $ So I'm a bit ...
0
votes
1answer
15 views

FOL - Predicates without quantifier

In First Order Logic if we take the predicate symbol greater,then the formula greater(5,3) is a well-written formula. If I ...
0
votes
0answers
8 views

P.r. Properties, Computability, Arithmetic [on hold]

How it is possible to show that the property “x is an open term”, namely Term(x), is primitive recursive using a Gödel coding scheme. Thanks!!
1
vote
0answers
21 views

Structure satisfiability and entailment

Let $Fv[\phi]$ be the free variables of $\phi$. Suppose there are 2 formulas $A,B$ such that $Fv[A] \subseteq \{x,y\}$ and $Fv[B] \subseteq \{x,y\}$. Prove/Disprove: $T \nvdash A\wedge B$ iff ...
0
votes
2answers
23 views

Expressing interrelationships in first order logic

I'm trying to figure out how to best formalize the following interrelationship in first order logic: a material has (electric) resistance $r$ and conductance $g$, and the two are related as $r \cdot g ...
1
vote
2answers
54 views

How are quantifiers managed in truth tables?

How are quantifiers ($\forall$ and $\exists$) managed in truth tables? I'm not actually sure it would make sense to include them in truth tables, but I can't exactly say why either. For example, ...
0
votes
0answers
35 views

Converting formula to a closed form with only existential quantifiers

Let there be some formula $\phi$, is there an algorithm to construct a closed formula $\phi'=\exists x_1...\exists x_n \psi$ where $\psi$ does not have any quantifiers and $\phi$ is satiable iff $\phi'...
1
vote
0answers
12 views

Ehrenfeucht-Fraisse games and first order formulas in one free variable

I've been reading lately Martin Otto's proof of Van Benthem - Rosen theorem. This theorem states that first order formula in one free variable $\alpha(x)$ (in vocabulary of Kripke structures, that is: ...
0
votes
0answers
19 views

About independence of sentences from a given set of axioms

Assume $\text{Sat }\Phi $. $\phi$ is independent of $\Phi $ iff $\text{not Sat } \Phi \cup \{\phi\}$ and $\text{not Sat } \Phi \cup \{\neg \phi\}$. Above definitely doesn't make sense as taking any ...
1
vote
0answers
30 views

Type amalgamation

Definition Let $\mathscr{L}$ be a first-order language and let $\mathcal{K}$ be a class of (possibly finite) $\mathscr{L}$-structures. $\mathcal{K}$ is said to have amalgamation property (AP) if for ...
2
votes
2answers
43 views

Types and automorphisms in model theory

Let $T$ be a first order theory and $\mathcal{M}\models T$ and let $A\subseteq M$ and $\bar{a},\bar{b}\in M^n$. Question. Is the following statement always true and why? $$\text{tp}^{\mathcal{M}}(\...
2
votes
1answer
45 views

How to create models in First-order logic

I'm a bit confused when it comes to defining models in First-order logic (FOL). Before I ask my question I thought I would show the semantics of how I create them and if I have understood it correctly ...
1
vote
1answer
33 views

Converting a FOL formula to a predicate only version

Suppose there are 2 signatures: $ \sigma_2= \{c, f^1, =^2 \}$ where $c$ is a constant, $f$ is a function symbol of arity 1, and $=$ is a predicate symbol of arity 2. Also, $\sigma_1 =\{R^2,P^1, =^2 \}$...
1
vote
2answers
41 views

How should logic notations be used when solving an equation?

This is what I found in one of my books (High school books; so probably not very mathematically accurate): I believe that the calculation itself is accurate; however, regarding the logic notations ...
8
votes
3answers
163 views

Where are the model theory concepts from?

Look at the following definition. Definition. Let $\kappa$ be an infinite cardinal. A theory $T$ is called $\kappa$-stable if for all model $M\models T$ and all $A\subset M$ with $|A|\leq \kappa$ we ...
2
votes
1answer
18 views

Showing via Ehrenfeucht-Fraïssé games that acyclicity is not definable in FO for finite graphs

I've been working through Elements of Finite Model Theory (Leonid Libkin) and am stuck on exercise 3.4. As in the title, the question asks "Using Ehrenfeucht-Fraïssé games, show that acyclicity of ...
1
vote
1answer
25 views

Domain size constraint on satisfiability

I need to prove whether the following statement is true or false: let $L$ be a first order language with the following signature $\sigma = \{{p_1, p_2, p_3}\}$ which are all 1-ary predicates. Does ...
1
vote
1answer
44 views

Predicate logic, models

I'm trying to understand predicate logic and models. I have an old exam question where we are supposed to find a model that shows that the formula does not hold: $$ \exists x(P(x) \land \neg M(x)), \ ...
2
votes
0answers
88 views

Translating from First Order Logic to Order-Sorted Logic

The following single sorted FOL sentences are from Stanford. Sorts or types are represented by predicates (e.g. $Horse(x)$) \begin{align*} &(1a) \forall x, \forall y ((Horse(x) \land Dog(y)) \...
2
votes
3answers
85 views

How can this implication be true? “$1>2 \ $ implies $ $ 'vegetables are healthy'.” [duplicate]

In mathematical logic, implication has the following truth table where $\phi$ and $ \psi$ are statements, and $1$ represents true and $0$ false. From this table, an implication such as "$1>2 \ ...
4
votes
1answer
97 views

Constructibility of uniquely defined sets in ZFC.

I was thinking about constructible universe, and I had the following idea. Suppose we have a predicate $\phi$ defined in a language of set theory. Suppose moreover, that the statement "there exists $...
1
vote
1answer
36 views

Quantifying a free variable in an example from “How To Prove It” by Velleman

This is an example from How To Prove It by Daniel J. Velleman (2nd Ed., p. 71): Example 2.2.3. Analyze the logical forms of the following statements. Statements about the natural numbers. ...
3
votes
1answer
68 views

“There is only” in first order logic

I'm trying to translate the statement "There is only three things that are not small" into first order logic. I'm using some software to verify my sentences, but I feel like I don't understand what "...
3
votes
4answers
64 views

Why is $∧$ used in the right-hand side of $¬(∀x, P(x) → (Q(x) ∧ R(x))) ≡ ∃x, P(x) ∧ (¬Q(x) ∨ ¬R(x))$?

According to my textbook, the negation of $\forall x, P(x) \to (Q(x) \land R(x))$ is $\exists x, P(x) \land (\lnot Q(x) \lor \lnot R(x))$, so $\lnot(\forall x, P(x) \to (Q(x) \land R(x))) \equiv \...
7
votes
2answers
676 views

Are these formal formulas equivalent?

My textbook gave the following $ \forall x_0 (\exists x_1 \ x_0=(\mathbf{O''} \cdot x_1) \vee \exists x_1 \ x_0=((\mathbf{O''} \cdot x_1)+\mathbf{O'})) $, then commented on the syntax and why the ...
6
votes
2answers
79 views

How do I properly use a logical implication sign when solving an equation?

I was reading a book on mathematical logic, and I was confronted with the following question: $ $ $\sqrt{2x+1}=\sqrt x-5 ⇒ 2x+1=(\sqrt x-5)^2$ $⇔ 2x+1=x-10\sqrt x+25$ $ ⇔ 10\sqrt x=24-x$ $ ⇒ ...
10
votes
4answers
167 views

Problems teaching introductory logic. Is this a statement? “If x is an integer, then…”

Consider the claim, "If $x$ is an integer, then $x^3>0$". Is this a statement? My text defines a statement as "a declarative sentence which is true or false, but not both." At first it seemed ...
2
votes
2answers
98 views

Doubts about Goedel Completeness Theorem

My book (Mendelson) states this theorem the following way: (1) A logically valid formula of a first order theory is a theorem. On Wikipedia the statement is a little more general: (2) For any ...
1
vote
1answer
44 views

Mathematical Induction: First vs. Second order Induction Axiom

The second-order variables in the second order Induction Axiom of (second order) Peano Arithmetic range over the set of all subsets of the natural numbers, that is, it has uncountable cardinality. ...
2
votes
1answer
62 views

What if someone comes up with a proof of consistency of arithmetic under the following conditions?

Suppose that one day, someone comes up with a proof of consistency of Peano arithmetic (PA) within itself. Then, does it mean that PA is actually inconsistent? Because, by the Gödel's incompleteness ...
5
votes
1answer
46 views

Research areas in Peano arithmetics

So I recently just finished a course on Peano arithmetics and it's non-standard models. I am very much intrigue by this topic. Hence I am rather curious what are some research areas surrounding PA ...
2
votes
0answers
35 views

Translation of infinite-valued QBF to first order logic

Quantified Boolean Formulas with infinite values are distinct from their usual 2-valued version (proof). Is there a known way to express such formulas in standard first order logic notation (so that ...
4
votes
1answer
48 views

Proving something about an object by expressing it as an ultraproduct of easier to understand objects

I was looking at this proof of the Ax-Grothendieck theorem, the theorem that any injective polynomial function on $\mathbb{C}^{n}$ is surjective. The conclusion of the Ax-Grothendieck theorem is, in ...
2
votes
1answer
65 views

The theory of infinite abelian group of exponent $p$ is model-complete

This is exercise 2.16.10 in Kenneth's Foundation of Mathematics. How to make use of the hypothesis the group is of exponent $p$ to prove that the theory of infinite abelian group of exponent $p$ is ...
1
vote
1answer
61 views

Is it possible to have equality in the body or head of the implication of the first order logic?

I am confused a bit, is the following formul a syntactically valid formula of first order logic? ...
1
vote
0answers
30 views

Meaning of a first-order logic theory

I'm wondering what results are typically used to show that a first-order logic theory captures its intended meaning. To make things concrete, suppose I have a signature $\Sigma = \{ 0, S, =, +, \leq \...
3
votes
1answer
71 views

Reconstruction of FOL language

If we have a FOL language $S$ and we suddenly lost its logical structure $\left(\rightarrow,\wedge,\vee,\bot,\top,\forall x,\exists x\right)$, can we recover it (modulo a logical equivalence) using ...
1
vote
1answer
52 views

Independence and Consistence of Formal Systems

Let $S$ be a formal system with axioms $A,A_1,\dots,A_n$. The system $S$ is said to be consistent if no contradiction can be proved (i.e. we can’t prove both a formula and its negation). If $S$ is ...
2
votes
1answer
52 views

Which one of the following equivalence is wrong [closed]

$$ 1) \forall z \ C(z,y) \ → B(t) \iff \forall z \ ( C(z,y) → B(t)) $$ $$ 2) \forall z \forall u \ (\forall x \ A(x,u) → \forall x \ B(x,z)) \iff \forall x \forall u \ A(x,u) → \forall z \forall x \ B(...
0
votes
1answer
100 views

Let P and Q represent formulas. Would stuff like $(P \wedge \neg P) \models Q$ make sense?

I confess, I am in a state of total confusion right now. And I am still struggling to grasp the underlying distinction between the normal material implication, $\Rightarrow$, and the notion of ...
1
vote
1answer
57 views

Logical Formalization of: “Children don't eat pasta with spinach or mushrooms on it”

I want to formalize the following sentence in predicate logic: If a children has spinach or mushrooms on its pasta then it will not eat its pasta. The headline contains a shorter version. I have ...
2
votes
0answers
30 views

Illegal Herbrand Logic sentence

I am studying the Stanford Introduction to Logic course. There was a problem about whether an expression is legal sentence of Herbrand Logic or not. It asks: Say whether $p(f(p(a))$ is a ...
4
votes
1answer
60 views

is first-order logic with constants equally expressive as first-order logic without constants?

I define a logic as a set of formulas $\mathcal{L}$ (formulated in some given signature) with a consequence relation $\vDash$. Say a logic $L_1$ is at least as expressive as $L_2$ if there is a ...
3
votes
5answers
124 views

How to prove $2+2=4$ using Zermelo–Fraenkel Set Theory?

I'm familiar with the famous excerpt from Principia Mathematica by Bertrand Russel and Alfred Whitehead. However, as Zermelo–Fraenkel Set Theory is today's most used foundation of mathematics (or ZF ...
0
votes
1answer
50 views

Prove the theory of equality with a finite number of unary predicates is decidable

Let the signature have $n$ unary predicate symbols $P_1, \dots, P_n$ and a single binary predicate $=$. Consider the theory of equality with the following axioms: $\forall x (x = x)$ $\forall x \...
0
votes
0answers
36 views

checking validity of given first order logic

Apologies if this question is already posted.As it is hard to search $\LaTeX$ in google and first order logic in nothing without $\LaTeX$ .But i am sure i have different doubt than that of already ...
3
votes
2answers
34 views

Which of the following logic statements are true

Question $S_1: \,\,\forall x \,\exists y \, \forall z\,(x+y=z)$ $S_2: \,\, \exists x \, \forall y \, \exists z\,(x+y=z)$ where $x,y, \text{and} \,\,z $ are real numbers. Which of the ...
1
vote
0answers
60 views

Spivak's Calculus Exercise 2-9

This is exercise 2-9 from Spivak's Calculus: Prove that if a set $A$ of natural numbers contains $n_0$ and contains $k + 1$ whenever it contains $k$, then $A$ contains all natural numbers $> n_0$...
0
votes
0answers
23 views

Can truth of a single predicate be defined by another language that only shares that predicate?

I have been looking at Tarski's work and asked a question here: Can truth be defined by a 'same-level' language according to Tarski's undefinability theorem? I am trying to refine my ...