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

learn more… | top users | synonyms

1
vote
0answers
28 views

Prove/Disprove: a clause $\exists xA$ is true in structure $M$ iff there is a term without FV such that $A\{\frac{t}{x}\}$ is true in $M$

Prove/Disprove: Let $M$ such that for every $a\in D$ (the domain) there's a term $t$ such that $t\mapsto a$,in $M$. Claim: a clause $\exists xA$ is true in $M$ iff there is a term without free ...
2
votes
3answers
64 views

Logical limitations of Proofs by Contradiction

In general proofs by contradiction go as follows: Given an arbitrary hypothesis, $\ p \implies q$, we assume $\left(p\implies q\right) = T$, and then we show that by assuming the hypothesis to be ...
-4
votes
0answers
18 views

prove the proposition using formal logic [closed]

prove using formal logic $\forall x ( \neg P(x) \lor Q(x)) \vdash \forall x ( \neg H(x) \lor Q(x)) \lor \exists x ( H(x)\wedge \neg P(x))$
0
votes
0answers
23 views

proof : the set of all logical consequences $S,\{F:S \models F\} $ is a maximal set. [closed]

prove that the set of all logic consequences $S,\{F:S \models F\} $ is a maximal set.
2
votes
0answers
64 views

Is Leibnizian calculus embeddable in first order logic?

We just published an article making what we feel is a plausible case in favor of an affirmative answer in Foundations of Science, see preprint here. The basic argument is that while such a requirement ...
1
vote
0answers
20 views

Deductive closure from Completeness

the prompt asks to show that if $\Sigma$ is complete, then it is deductively closed. I know that deductive closure means $\Delta \vdash \sigma$ implies that $\sigma \in \Delta$. and that since ...
0
votes
1answer
51 views

Deductive Closure as intersection of all Sets of sentences that are true in a Structure?

A set $\Delta$ of Formulae is deductively closed iff $\Delta$ $\vdash$ $\sigma$ implies that $\sigma$ $\in$ $\Delta$. $\Gamma$ is a set of sentences. Define $\Sigma_{\mathcal{A}}$ as all sentences ...
1
vote
0answers
18 views

Skolemization algorithm for a formula

I'd like to know if I my Skolemization is right: $$(\exists x(P(x)\lor R(x)))\to((\exists xP(x))\lor(\exists xR(x)))\\(\exists x(P(x)\lor R(x)))\to((\exists yP(y))\lor(\exists zR(z)))\\(\exists ...
2
votes
2answers
37 views

Is the universal quantification symbol $\forall\;$ known as “for any x” or “for all x” in First Order Logic & why is this different to Discrete Math?

I'm reading a book by Mark Tarver called Logic, Proof and Computation. Chapter 8 (starting p71) is about First Order Logic. On page 77 (of Chapter 8) the author writes: For any value for 'x', in ...
17
votes
3answers
1k views

Why does what I've written fail to define truth?

I stumbled across a set of axioms for first order logic a bit ago. Intrigued, I decided to try to write it all down and organise what I read. After I did that, it seemed to me as though one could ...
0
votes
1answer
40 views

Binary resolution: how to prove that it is not complete in FOL

My question is very simple: how can I prove that binary resolution is not complete in First-Order Logic? I have found a first attempt of explaination by means of counterexample in which I have: ...
0
votes
0answers
28 views

How to Prove? - If the interpretation of theory is consistent, then the interpreted theory is consistent

Let L1 and L2 be finite or recursive languages, and T a theory in the language of L2. A translation of L1 into T is an assignment to each sentence S of L1 into a sentence i(S) of L2 such that: (T0) ...
0
votes
3answers
61 views

Deductive proof - need help, explanation how to

I am working on assignment for school where the task asks to give a deductive proof. However, I have never used this technique (nor that I am very good in proofs in general) thus it is quite ...
2
votes
0answers
29 views

Describe a set with FOL formula

This is a problem from Introduction to Mathematical Logic course A structure $\mathscr{A}$ with domain $\mathbb{N}^k$ is for FOL language $\mathscr{L}$ with $k$ predicate symbols $p_1, \ldots, p_k$ ...
0
votes
2answers
40 views

Why does a finite set having a model imply that the set is consistent [closed]

Assuming the soundness theorem to be true, can someone explain why if we assume $\Sigma$ has a model $M$. Then $\Sigma$ is consistent ?
1
vote
2answers
32 views

First order structures for Posets

Im tackling this question: So Im ok with part (a) For part (b) I came up with $\sigma_n :=\exists x_1 \exists x_2 ... \exists x_n \Bigg(\bigwedge_{i\neq j}\Big(\neg (x_i\leq x_j)\wedge \neg ...
0
votes
2answers
23 views

Rectified prenex form conversion algorithm inconsistencies

I've looked at these two different RPF conversion algorithms where the first step of each, say 1 and 1', states: 1.Remove all “$\to$”s using the fact that $\alpha\to\beta ≡ \neg\alpha\lor\beta.$ ...
1
vote
0answers
14 views

Nested FOL formulae

Is there a GENERAL FOL formulae to represent nested expression? Example: A(x) ∧ B(x) ∧ (C(x) ∨ D(x) ∨ ( ¬ E(x) ∧ F(x) ) ∨ G(x) ) ∧ ¬ H(x)
1
vote
1answer
28 views

Interpreting a first order sentence

I've been given this first order sentence with a binary relation symbol $R$: $\forall x \exists y (R(x, y) \land \forall z(R(x, z) \implies (R(y, z) \land (y=z)) ) $ We are then given two ...
0
votes
0answers
27 views

First Order Logic Tableau Multiple Universal Identifiers

I've been looking into tableau lately and I have come across multiple Universal Identifiers which I am not used to. How do I approach these to validate/invalidate with these identifiers and provide an ...
1
vote
2answers
61 views

Prove that, for any sentence A of the predicate calculus with identity, at least one of spectrum(A) and spectrum(¬ A) is cofinite

I got the following exercise: Prove that, for any sentence A of the predicate calculus with identity, at least one of spectrum(A) and spectrum(¬ A) is cofinite. I already tried to prove this ...
1
vote
1answer
30 views

Why does the undefinability proof fail for $\mathbb{N}$ in $(\mathbb{Z}, 0, <)$?

An exercise asks to prove that: $\mathbb{N}$ is not definable in $(\mathbb{Z}, <)$, but definable in $(\mathbb{Z}, 0, <)$ (in the first-order logic). The solution to the former one relies ...
0
votes
0answers
11 views

Is this First Order Formula correct?

I'm trying to write a FOL formula that produces all unary predicates with arbitrary ∧ ∨, e.g. a ∧ b ∧ c ∨ d ∨ e ∧ f ∨ g ∧ h ∧ i. The point is that I use the ...
2
votes
1answer
20 views

How to prove: If $(\omega, <) \equiv \mathcal{M}$, then $(\omega, <) \prec_{f} \mathcal{M}$

To prove that If $(\omega, <) \equiv \mathcal{M}$, then there exists a function $f: \omega \to M$ (the domain of $\mathcal{M}$) such that $(\omega, <) \prec_{f} \mathcal{M}$. where, the ...
0
votes
2answers
18 views

Is direction of logical consequence in FOL arbitrary?

Wikipedia says about logical consequence: A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically ...
0
votes
0answers
22 views

Modelltheory, validity of a formula

I have a question to the following task: $M=\{1,2,3\}$ and $R=\{(1,2),(1,3)\}$ Let $\mathcal{L}$ be a first order language with a binary relationsymbol $\overline{R}$ so, that $\mathcal{M}=(M,R) is ...
0
votes
1answer
19 views

Skolemization problem:∀x∃y∀z∃u (A(x,y,z,u) v B(y,u))

Everything in the title but an explanation would be nice beside an answer! I don't really know if I should use constants or functions.
0
votes
1answer
23 views

Entailment in first-order logic using resolution

I have the following sentences in the KB: 1) (¬Y(x) v F(x)) ^ (¬Y(x) v D(x) v C(x)) 2) Y(something) 3) ¬C(x) v L(x) 4) ¬D(x) v L(x) And am trying to find if the ...
0
votes
1answer
19 views

Can you use constants from the domain in a First Order Formula? [closed]

Say I have a First Order Signature defined like so: $N = (\{1,2,3\dots\},T)$ Where T is a binary relation symbol. Can I use values from the domain to define functions over this signature? For ...
0
votes
1answer
25 views

Formal proof fitch-form

[![enter image description here][1]][1]Hi I am trying to produce a formal proof to prove Cube(a) from premises 1 and 2 as show below. It allso shows what I got so far but Im very stuck. Am I correct ...
0
votes
1answer
32 views

Exercise in Peano Arithmetic

I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah. I'm doing exercise about Peano Arithmetic and I have to show that: $\vdash(\forall z\leq x(z\geq 1 ...
2
votes
2answers
66 views

Prove that: $\vdash \forall x \exists !y(y=x)$

Prove that: $$\vdash \forall x \exists !y(y=x)$$ in first order logic. The first thing to do would be to write this as $$\forall x (\exists y(y=x) \land \forall y\forall z (y=x \land z=x \to y=z))$$ ...
1
vote
1answer
42 views

Prove that: $\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$

How does one prove that $$\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$$ in first order logic? I have tried using the specialization and generalization rules on various wffs ...
0
votes
1answer
24 views

Prove that it is a theorem

I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah. I'm doing exercise about Peano Arithmetic and I have to show that: $\vdash p|x \wedge r·s=p \to ...
0
votes
1answer
25 views

Give a derivation in Peano Arithmetic

I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah. Show that: $\vdash \exists y[y>1 \wedge \forall z(z\leq 0\wedge z>1\to z|y)]$ Hint: Show that ...
0
votes
0answers
38 views

How do I prove that $\vDash \alpha \to \forall x\alpha$, if $x$ is not free in $\alpha$

In First order logic, how do I prove that $\vDash \alpha \to \forall x\alpha$, if $x$ is not free in $\alpha$ Also, why is the condition that "$x$ is not free in $\alpha$" needed? This question ...
3
votes
2answers
26 views

Properties of an elementary substructure

Let $M$ and $N$ be structures for a first order language $L$, with $M$ an elementary substructure of $N$. This means that $M$ is a substructure of $N$ and if $\varphi(x_1,\ldots,x_n)$ is a formula ...
1
vote
1answer
32 views

Are those formulas valid?

Consider the following formulas: $\forall x(A\to B)\to ((\exists x A) \to \exists x B)$ $\forall x(A\to B)\to ((\forall x A) \to \forall x B)$ Now, I claim that both formulas are indeed valid. ...
0
votes
1answer
19 views

Help with using universal instantiation/generalization when variable ocurrence is unknown.

For example: $\forall x(\varphi \land \psi)\rightarrow (\forall x\varphi \land \forall x\psi)$ Now I would try to drop the forall, and deduce $\varphi$, $\psi$ from $(\varphi \land \psi)$ and then ...
10
votes
4answers
523 views

What's the point of allowing only quantification of variables in first-order logic.

In first-order languages, ${\forall}$ is allowed to quantify only over variables, so that ${\forall}v(P)$, where $v$ is some variable and $P$ is a WFF is the only kind of a WFF concering universal ...
1
vote
2answers
56 views

What does “Wenn $x$ frei für $t$ in $\phi$” mean?

The (German) text reads further Wenn $x$ frei für $t$ in $\phi$, dann $$\vdash_L \forall x \phi \rightarrow \phi \frac{t}{x}$$ The für and in are confusing me. (I am looking for an ...
0
votes
1answer
46 views

First order logic equivalence proof

I have this homework problem that I can't figure out. I have to show that the following sentences are equivalent: $\neg \forall c\; A(c)\Rightarrow\exists d\; B(d) \land \neg C(c,d)$ $\exists c\; ...
1
vote
1answer
29 views

Show a formula is satisfiable

Show that the following formula is satisfiable: $$(R(c)\land \forall x (R(x)\to R(f(x))))\to \forall xR(x)$$ here, $R$ is a relation and $f$ is a function. Now, if $R(c)=f$ then it easy to show ...
0
votes
2answers
19 views

First Order Logic and equivalence rules

I have a couple of questions about first order logic equivalence rules. How do you distribute the $\neg$ correctly with the $\exists$ and $\forall$ quantifiers? If let's say I have $$\neg[\forall ...
1
vote
1answer
56 views

What is a universal function in model theory?

What does it mean that a function in a model is universal? Let A be the domain of a model. As I understand it, an empty function is a function that is not defined for any object in A; an empty n-ary ...
1
vote
2answers
19 views

If $Mod(T_1 \cup T_2) = \emptyset$ then for some $\sigma$, $T_1 \vDash \sigma$ and $T_2 \vDash \neg \sigma$

Problem description: if $T_1$ and $T_2$ are theories such that $Mod(T_1 \cup T_2) = \emptyset$, then there is a $\sigma$ such that $T_1 \vDash \sigma$ and $T_2 \vDash \neg \sigma$. I don’t ...
0
votes
1answer
30 views

drawing tableaus for predicate logic?

I'm a bit confused about the rules. I know for existential ones, you replace the variable with a new constant and for universal you replace it with a closed term. $\forall x A(x) \to A(t)$ if $t$ is ...
1
vote
0answers
27 views

Can we prove undefinability theorem first (using techniques that are different from Godel's) and then deduce Incompleteness from it?

I asked a related question about the matter here in philosophy platform where it was suggested to ask a modified version of the question on Math.se My question is, Is there any known way to prove ...
0
votes
1answer
42 views

Why include equality in FOL for ZFC?

What are the pros and cons of working with first-order logic with equality for constructing ZFC, when all you have to do is make '$x=y$' a shorthand for: $$'\forall z [z \in x \Leftrightarrow z \in y] ...
0
votes
2answers
44 views

Show that well-ordering is not a first-order property.

Problem description: Show that well-ordering is not a first-order notion. Suppose that $\Gamma$ axiomatizes the class of well-orderings. Add countably many constants $c_i$ and show that $\Gamma \cup ...