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

learn more… | top users | synonyms

0
votes
0answers
30 views

a problem about truth in first order logic [on hold]

Suppose that $L$ is a first order language with no function symbol,constant and $=$ & $A=\forall x_1 \ldots x_n \exists y_1 \ldots y_m B$, $B$ has no quantifier.prove that $\models A$ if and only ...
2
votes
1answer
19 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
18 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
20 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
18 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
22 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
28 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
63 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
39 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
37 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
24 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
30 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 ...
9
votes
4answers
509 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
55 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 ...
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
54 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
18 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
40 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
37 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 ...
1
vote
1answer
37 views

Natural Deduction proof: ∀x¬∀y(Pxy→Qxy)⊢∀x∃yPxy

I'm trying to prove the claim ∀x¬∀y(Pxy→Qxy)⊢∀x∃yPxy in a Gentzen-style system. I know that I will have to use universal elimination to derive ¬∀y(Pay→Qay)from ∀x¬∀y(Pxy→Qxy). I would then use ...
0
votes
1answer
13 views

How does a subset of a $\mathfrak B$-structure (which is a tuple) look like?

In our book, first order logical structures are defined as pairs $\mathfrak A = (A,(Z^{\mathfrak A})_{Z\in L})$, where $L$ is a signature, and A is the underlying set/carrier of $\mathfrak A$. ...
1
vote
1answer
53 views

Completeness Theorem in logic and Completeness of a theory

Completeness Theorem says: $\Gamma \models \phi \longrightarrow \Gamma \vdash \phi$ And from definition of satisfaction: $\neg(\Gamma \models \phi) \longleftrightarrow \Gamma \models \neg\phi$ Now ...
6
votes
2answers
82 views

Is the axiom of induction constructively verifiable for a non-standard model of Peano arithmetic?

There exist models of the natural numbers which include infinite numbers. Such models are called non-standard models of arithmetic. (Proof: by the compactness theorem, there exist models of Peano ...
0
votes
1answer
6 views

Reachability and first-order logic

I am trying to understand why directed graph reachability cannot be expressed in first-order logic. In Papadimitriou's "Computational Complexity" book this is proven by contradiction. Assume that ...
0
votes
0answers
7 views

How do I use resolution refutation in backward reasoning

Suppose I have the following facts in my KB: ∀a,b: g(a,b)→ p(a,b) ∀x: ¬p(x,x) ∀x,y,z: p(x,y)∧ p(y,z)→ p(x,z) ∀w,r: p(w,r)→ g(w,r) I have a questions: If I want ...
3
votes
0answers
51 views

Is there a name for this principle of logic? From $\exists a P(a), !bQ(b), \forall a(P(a) \rightarrow Q(a)),$ infer $\forall a(Q(a) \rightarrow P(a))$

In set theory, we have the following: Observation 0. Let $X$ denote a set. Let $A$ and $B$ denote subsets of $X$. Then if $A$ has at least one element, $B$ has at most one element, and $A ...
1
vote
1answer
26 views

How to evaluate truth of expressions with free variables?

I'm learning FOL, and in the book I'm reading, I found an exercise containing a logical expression which should be evaluated to true/false, though I can't see how it would be possible. The exercise ...
0
votes
0answers
28 views

Formalising a problem given in natural language into predicate logic

I am working on a research paper and I want to formalise the problem which we tackle and process for solving it using predicate logic. I used predicate logic in the past for formalising simple ...
1
vote
2answers
45 views

Definability of the $<$ order relation on the natural numbers using addition. [closed]

Show that the usual order relation $<$ on the natural numbers is definable in the structure $(\mathbb{N}, +)$ with only addition. My teacher has clarified this for me and quantifiers can be used. ...
3
votes
2answers
45 views

Prove that there exists a sentence $\varphi$

I'm doing some excercises from the book "The Incompleteness Phenomenom" from Goldstern and Judah. I have to do this and I don't know how to start. Let $\Sigma_1 $ and $\Sigma_2$ be sets of sentences ...
0
votes
1answer
38 views

Use of quantors/quantifiers and variables in first-order logic.

Let $v_1,v_2,\dots,v_n$ be variables and $\beta$ the variable assignment $\beta(v_n)=2n$ for $n\geq 0$. Of the following, which are true and which false under $\beta$? $\forall v_0 \exists v_1 ...
1
vote
1answer
32 views

translating uniqueness quantifier algorithmically

Given a claim with a uniqueness quantifier $\exists$!, such as: $$\forall x \exists!y \ P(x,y) $$ A standard translation that uses $\forall$ and $\exists$ only (there are several possible ones) is: ...
0
votes
2answers
55 views

Differentiating between standard and non-standard interpretations of 'less than' relation

Take a relation $R$. In Structure $A$, $R$ is interpreted as the 'less than' relation (for natural numbers). In $B$, $R$ is interpreted as a relation (for natural numbers) where $R(a,b)$ holds if and ...
0
votes
0answers
13 views

Prove that there is a syntactic equivalence for a formula with repeated occurrences of a quantifier

A formula $A$ has repeated occurrences of a bound variable $x$, if $Qx$ appears more than once in the sub-formulas of $A$. Here $Q \in \{∀,∃\}$. Prove that there exists a formula $B$ which has no ...
1
vote
3answers
91 views

In relatively simple words: What could be a model of $\sf {ZFC}$?

An $\text{interpretation}$ of a theory consists of A domain of discourse $\mathcal U$, usually required to be non-empty. For every constant symbol, an element of $\mathcal U$ as its ...
2
votes
2answers
27 views

Predicate Logic: Distinguishing structures in the first-order language having only multiplication

I am attempting to distinguish the below structures under the multiplication function. As of right now I have determined the following: <N, ⋅>|= ∃z∀x∀y ((x-x=z)∩(y-y=z)) (xy ≥ z) ...
2
votes
2answers
79 views

Valid inference in first-order predicate logic

I should prove for the following premises and conclusion if the inference/conclusion is valid by using general resolution for clauses. The conclusion is valid if it is possible to derivate a ...
2
votes
2answers
60 views

About ZFC, peano's axioms, first oder logic and completeness?

I read somewhere that the peano's axioms can be derived out of ZFC. But if that is the case ZFC would be incomplete right( by Godel's incompleteness theorem)? But since ZFC is in first order logic , ...
0
votes
1answer
16 views

Formalizing the definition of continuity and uniform continuity according to first order logic

To be clear, I am familiar with the whole concept of continuity and uniform continuity, I'm just struggling with the formalization of the two statements. I get that in considering the differences of ...
1
vote
4answers
77 views

Say we have a presentation of a finite group. Does adding additional relations to the presentation always decrease the size of the group?

It seems like it should, but I'm not sure how to prove it. EDIT: I'm talking about nontrivial new relations here, i. e. ones that do not follow directly from the old ones.
0
votes
3answers
61 views

Construct formal proofs using the natural deduction

So I'm currently studying First Order Logic, and I'm really struggling with constructing formal proofs. I managed to solve some of the basic problems, but can't seem to understand this one. Can you ...
5
votes
1answer
99 views

I don't really understand what a model is.

I've studied a bit of first order logic, and I still don't understand what a model really is. A model of a theory $T$ is an interpretation which assigns the value True to its sentences. Ok, ...