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

learn more… | top users | synonyms

0
votes
1answer
26 views

Use Resolution to proove a sentence in First Order Logic

I was just wondering if anyone could tell me if I've solved this problem right. If wrong, I would like to know what I did wrong. "Use resolution to prove Green(Linn) given the information below. You ...
1
vote
1answer
47 views

Given $x,y\in\mathbb R$ is there a “formulaic” way to obtain a $q\in\mathbb Q$ with $a<q<b?$

Is there an assignment of reals $x,y$ to a rational number $q(x,y)$ for which $$\forall_{\mathbb R} x.\forall_{\mathbb R}(x<y).\left(x<q(x,y)<y\right)\hspace{.2cm}?$$ For computable reals, ...
2
votes
2answers
36 views

How would you prove in FOL that x is a member of {x} for all x?

How can I formulate and prove the following in first-order logic? $$\forall x (x\in \{x\})$$ I have the following two statements: member(x,$\alpha$) $\neg \exists y(\text{member}(y,\alpha )\land ...
0
votes
1answer
21 views

Language and Finite Models

Let us consider the language consisting of one symbol $R$ for a binary relation. Let $\sigma$ denote the following sentence: $\forall x \exists y \exists z \ x\neq y \wedge y \neq z \wedge x \neq z ...
1
vote
2answers
54 views

Consider $(\mathbb N, +)$ as a model for the language with one binary function $+$ . Are the following statements true?

Consider $(\mathbb N, +)$ as a model for the language with one symbol $+$ for a binary function. Are the following statements true? $(\mathbb N, +) \vDash \forall x \exists y \forall z\ x + y\neq z$ ...
0
votes
2answers
53 views

Let $\Gamma = \{\exists x \forall y (x\mathrel R y),\exists x \forall y(y\mathrel R x),\forall x\exists y(x\mathrel R y)\}$. Is $\Gamma$ consistent?

Consider the language consisting of one symbol $R$ for a binary relation. Let $\Gamma = \{\exists x \forall y (x\mathrel R y),\exists x \forall y(y\mathrel R x),\forall x\exists y(x\mathrel R y)\}$. ...
1
vote
1answer
36 views

Formal Proofs: $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$

I wish to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$ using the Hilbert System in First-Order Logic with the following axioms: Tautologies $\forall x \alpha ...
0
votes
1answer
35 views

Proof for $∃xA⇔¬∀x¬A$

I want to prove, that $∃xA⇔¬∀x¬A$, using classic axioms. I think, I have to start with the following step: $∃xA⇔∃x¬¬A$ But I do not know, how to make this step, using axioms: $∃x¬¬A⇔¬∀x¬A$
1
vote
2answers
61 views

Hilbert's style proof (FO logic)

I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. ...
1
vote
2answers
40 views

How to eliminate implications with quantifiers

I'm reading some stuffs on the conversion of a FOL sentence to CNF form. However, I'm stuck with this problem: why should this $$\forall x [\forall y Animal(y) \Rightarrow Loves(x,y)] \Rightarrow ...
1
vote
1answer
201 views

Formal Proofs: $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$

First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms: ...
0
votes
1answer
37 views

What does First Godel's Incompleteness theorem mean?

I am terribly confused what really "Incomplete" mean in terms of the Godel's theorem. Does it mean there are some theorems that are definable in First order theory of natural numbers and true but ...
0
votes
1answer
18 views

Why is $M\subseteq Mod(Th(M)) $?

In first-order logic, an immediate corollary of the definitions of the theory of a set of models M (denoted $Th(M)$) and the Model of a set of sentences S (denoted $Mod(S)$) is: $M\subseteq ...
0
votes
1answer
29 views

Are these structures in the same language?

I have these teo structures, $(N, <)$ and $(Q, <)$. And I want to know if they can come from the same language? I'm confused about the definition I have for an La-structure. Specefically about ...
2
votes
2answers
39 views

Different definitions for consistent set of sentences

In my logic class, we were given the following definition for a set of sentences being consistent in first order logic: Let $\Gamma$ be a set of sentences in some underlying language $L$. The set ...
4
votes
1answer
52 views

If $\Gamma \cup \{ \neg \varphi \}$ is inconsistent, then $\Gamma \vdash \varphi$

If $\Gamma \cup \{ \neg \varphi \}$ is inconsistent, then $\Gamma \vdash \varphi$ Here, a set of formulas is inconsistent means they syntactically imply some formula as well as its negation. ...
2
votes
1answer
62 views

Proof in First-Order Logic using Compactness Theorem

If we have $\Sigma$ and $T$ as two first-order theories such they do not have any common models. How can I prove that there is a sentence φ such that Σ ⊨ φ and Τ ⊨ ¬ φ? Does Compactness Theorem help? ...
1
vote
1answer
43 views

Impredicativity and set theory

I have thought about an example in set theory, but I don't know if its legal to do it, maybe someone can help. Let $\emptyset$ be given and let $A$ be a non empty set. Let us create the subset $X = ...
2
votes
1answer
36 views

Algebraic invariants for first order equivalence between fields

I know that every two models of the theory $ACF$ (namely two algebraic closed fields) with the same characteristic are elementary equivalent. But what about generic fields? Are there any algebraic ...
2
votes
1answer
35 views

If a wff is simply atomic (e.g. $Pxy$) are $x$ and $y$ considered free in it?

(Using First-Order Logic Hilbert System) I found the following "solution" to $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$: $\forall x \forall y Pxy \vdash \forall y Pzy$ (A2, MP) ...
1
vote
1answer
28 views

Use of model theory in flag algebras

I need to learn about Razborov's "flag algebras" (see http://bit.ly/1u1a1NB) to solve a problem about graphs. Flag algebras are a very general new algebraic tool for studying combinatorial structures. ...
2
votes
2answers
45 views

The symbol $\sigma[x/a]$ in mathematical logic

I've just started learning mathematical logic, and my teacher teaches in a very formal and unintuitive way. I'd like to know what meaning hides behind the symbols below: For an assignment $\sigma: ...
1
vote
1answer
53 views

Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$

We're in first-order logic, using the Hilbert system (with inference rule of modus ponens), and the problem is to show $\vdash \exists x (Px \rightarrow \forall x Px)$. We just learned about this ...
0
votes
1answer
40 views

Proof for $\forall x A \Leftrightarrow \neg \exists x \neg A$

I try to proof, that $\forall x A \Leftrightarrow \neg \exists x \neg A$ I know how to proof, that $\forall x A \Leftrightarrow \exists xA$, but I don't understand, how to get negation.
2
votes
1answer
113 views

How to define mathematical objects from scratch?

Are there any "Zermelo-type theories" for some other type of mathematical objects except for sets? I.e., axiomatic systems for mathematical objects formalized for first-order logic using a language ...
0
votes
1answer
47 views

Re-expressing a statement in First Order Logic in Propositional Logic

From what I understand a propositional variable must represent a statement (either true or false). If so, eliminating free variables from any predicate by either: (1) Replacing free variables with ...
1
vote
1answer
38 views

First-Order Language without any Constant, Function, or Relation

recently I saw an interesting problem from a textbook and wondering if there is any neat and elementary solution for it: For a language without any function, constant, or relation, how do we get a ...
2
votes
0answers
56 views

Non-forking frames in AEC

Here http://shelah.logic.at/files/875.pdf on page 15, item 4 in the proof of 2.2.6, I would like to know why $S(M)\leq \lambda \times \lambda^+$. I understand that models in $K$ have cardinality ...
0
votes
0answers
20 views

Principal ideal rings are not FO axiomatizable

A ring $R$ is a principal ideal ring if it is a ring and a model of $\forall I[I \text{ is an ideal} \to \exists x \forall y(y \in I \leftrightarrow \exists z (y = z*x))]$. How can one prove that this ...
0
votes
1answer
29 views

Deduction and universal generalization in FOL

I'm working on a problem in Enderton's A Mathematical Introduction to Logic, Section 2.4, but having some trouble. I need to prove that if $\vdash$ $\alpha$ $\rightarrow$ $\beta$, then $\vdash$ ...
1
vote
0answers
35 views

Relations between equations in a theory, and the number of independent equations

I have a question on equational reasoning in theories, which is made quite often in mathmeatics, and I am trying to make this more formal. So for my attempt to make this more rigouros, I choosed ...
10
votes
2answers
901 views

How to find the shortest proof of a provable theorem?

Roughly speaking, there are some fundamental theorems in mathematics which have several proofs (e.g. Fundamental Theorem of Algebra), some short and some long. It is always an interesting question ...
0
votes
1answer
70 views

Induction in a first order system with ZF

Suppose I have some characterization of the natural numbers $N$ in a first-order system under ZF. To be precise, I have $N = \lbrace n: \forall w:( w\space is\space inductive) \rightarrow n \in w ...
3
votes
1answer
45 views

defining inequality of natural numbers by case-analysis

If I add to Peano Arithmetic a relation (predicate?) symbol $\leq$ and an axiom $\forall n\forall m(n\leq m \leftrightarrow n=m \lor S(n)\leq m)$, can I prove $\forall n\forall m(n\leq m \to n\leq ...
0
votes
0answers
22 views

Need help converting first order logic predicate to Conjunctive Normal Form (CNF)?

Attempted to translate from first order predicate to conjunctive normal form, but I'm still worried that most of the translation is incorrect. Could someone please show me the errors that I did? I'm ...
0
votes
1answer
27 views

How are the following english sentences should be translated to first order perdicate logic?

I'm still confused with my first order predicate logic and I need to know what the correct translation would be for each of the English sentences to first order logic. Could anyone show me or give me ...
2
votes
1answer
55 views

How can universal quantifier manipulation rules be made redundant by the generalization rule (metatheorem)?

On the Wikipedia page for Hilbert style axioms, in the "Logical axioms" section, it gives the axioms to manipulate universal quantifiers : $Q5. \forall x(\phi)\rightarrow \phi[x:=t] $ $Q6. ...
0
votes
1answer
43 views

Problem in solving a logical Equivalence

Prove or disprove the following equivalence: $$ ∀x Px \wedge ∀x Qx \Leftrightarrow ∀x ∃y ( Px \vee Qy ) $$ I've tried it, but I do not know how to solve logical equivalences involving quantifiers.
1
vote
1answer
68 views

How to better understand “ x occurs free in a wff ” in first order logic?

On page 121 of Herbert Enderton's A Mathematical Introduction to Logic, the author gives a proof of the following example : If x does not occur free in $\alpha$, then $$ \vdash ( \alpha \rightarrow ...
0
votes
3answers
32 views

Examples of automorphisms on structures

For some structure $(M,I)$ with $M$ a set and $I$ the interpretation of the constants, functions, and predicates, what is an example of a such a structure such that for each $a$ of $M$ there are only ...
-1
votes
1answer
34 views

Automorphisms of $(\mathbb{R}, +)$ [closed]

Does the structure $(\mathbb{R}, +)$ have infinitely many automorphisms?
1
vote
2answers
34 views

Proving the completeness of a theory $\Gamma$

Given a set of sentences $\Gamma$ in a first-order-language $\mathcal{L}$, such that for all structures $\mathcal{A}=(A,\ldots)$ and $\mathcal{B}=(B,\ldots)$, if both $\mathcal{A}$ and ${\cal B}$ ...
3
votes
3answers
70 views

High school geometry proofs and first order logic?

I am a student of logic who recently came across two column geometry proofs which seem to be the bane of many a high-school student. My main question though, is that is there any way of doing these ...
0
votes
1answer
47 views

Any substructure of $(\mathbb{N}; 0, 1, +, \cdot)$ is itself

Consider a substructure $\mathcal{M} \subseteq \mathcal{N} = (\mathbb{N}; 0, 1, +, \cdot)$. Prove that $\mathcal{M} = \mathcal{N}$. EDIT: This result seems intuitively easy, but I'm having trouble ...
5
votes
1answer
47 views

FOL and Conjuctive Normal Form Conversion

I see the CNF from following firs order logic: $ \forall x [ \forall y [ \neg A(y) \vee B(x,y) \Rightarrow [ \neg \forall y B(y,x) ] ] $ is equivalent to : $ (A(f(x)) \vee \neg B(g(x),x)) \wedge ...
1
vote
1answer
12 views

Representing positive numbers in first order logic with the structure ($\mathbb{R},+,\cdot$)

The problem is to represent (in first order logic) the interval $[0, \infty)$ under the structure $\frak{R}$, whose universe is the real numbers. $\forall$ quantifies the real numbers and ...
1
vote
1answer
29 views

Why is Skolem normal form equisatisfiable while the second order form equivalent?

I asked in another question when is it appropriate to de-Skolemize a statement. The answer, I'm not sure I'm satisfied with yet, relies on a second order logical equivelance, but Skolem normal form ...
0
votes
1answer
22 views

Construction of $\exists x_i (\phi)$ in first order logic.

How do we construct $\exists x_i(\phi)$ where $\phi$ a formula from first order language by using: The logical symbols $(,),\neg,\to,\forall$ The variable symbols $x_i$
1
vote
1answer
43 views

Law of Excluded Middle

I'm here with a question about solving a premiseless proof in a blocks language. With a goal of $\def\Cube{\operatorname {Cube}}\lnot(\Cube(b)\land b=c) \lor \Cube(c)$, is it right to try to prove ...
4
votes
2answers
51 views

When is de-Skolemizing statements appropriate?

In first order logic we often convert prenex normal form statements to Skolem normal form statements to eliminate the existential quantifier: $\exists$x$\forall$y$\exists$z$\phi$(x,y,z) becomes ...