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
25 views

Showing validity of a formula in first order logic [duplicate]

So I'm trying to prove the validity of this formula and I am a bit lost, not sure how to start. I know generally speaking a valid formula is one where if all the premises are true, then the conclusion ...
1
vote
2answers
40 views

What would be an example of a tautology in first-order logic involving a definite sequence of quantifiers?

This question might be silly, but while teaching a tutorial as a TA, I suddenly had the need to bring up a tautological statement in first order logic that involved the quantifiers $\forall\exists\...
0
votes
1answer
17 views

Finding equivalent statements with quantifiers

Find equivalent pairs: a. $\forall x(P(x)\land Q(x))$ b. $(\forall x(P(x))\land (\forall xQ(x))$ c. $\exists x(P(x)\land Q(x))$ d. $(\exists x(P(x))\land (\exists x Q(x))$ Are ...
1
vote
2answers
32 views

Are those statements Tautology?

a.$$\forall x\forall y \exists z (x\neq y)\rightarrow (x\neq z)$$ b. $$\neg\exists x\forall y \forall z (x=y)\rightarrow (x=z)$$ To revoke a. we need to find a case of $(x\neq z)\land (x=y)$ and ...
1
vote
1answer
68 views

understanding a proof which uses induction on the length of a formula

This comes from Shoenfield's textbook Mathematical Logic. Here is the theorem and its proof: If $u_1,\dots,u_n, u_1',\dots,u_n'$ are designators and $u_1\dots u_n$ and $u_1'\dots u_n'$ are ...
3
votes
2answers
29 views

Contrapositive of the statement involving “for every” and “there exists”

I have a statement (∃x.(P(x) -> (∀y.P(y)))) I am trying to formulate and understand the contrapositive of the formula. ...
2
votes
0answers
25 views

Software for solving first-order logic

Is there any class of software that can help me with the following problem in first order logic: given $\phi$ a formula with a "hole" in it (a subformula which is undetermined) and a particular set of ...
0
votes
1answer
31 views

can you help me to transform ∀x FO logical formula to it equivalent ¬∃ formula?

i have this formula ∀x ∀y (A(x,y) V A(y,x) → B(x,c1) ∧ B(y,c2) ∧ c1≠c2) to the equivalent formula that start by ¬∃x ¬∃ y ? you will find the question here ...
7
votes
1answer
87 views

Is $\pi = 3.14159…$ first-order definable in the reals?

Given first-order logic with equality and the real field $\mathbb{R} = (R, 0, 1, <, +, \cdot)$, is $\pi$ first-order definable? By first-order definable, I mean a sentence of the form $\exists x \;...
0
votes
1answer
25 views

True or falsehood of open formula under a fixed interpretation

Given the open formula: $\alpha =(\exists{{x}_{2}})({P}^{1}({x}_{1},{x}_{2}))$ And consider the interpretation $I$ where the domain is the natural numbers, and ${P}^{1}$ means equality. Is $\alpha$ ...
0
votes
1answer
26 views

Using separators as functional symbols in first order logic

Suppose we have the following definition of a term: A $term$ is: $x$, where "$x$" is a variable $c$, where "$c$" is a constant symbol $f(\tau_1,...,\tau_n)$, where "$f$" is a ...
1
vote
0answers
17 views

Citations for the proof of universality of graph classes

In Automorphisms of graphs, Peter J. Cameron mentioned following classes of graphs which are universal structures. graphs of valency k for any fixed k > 2; bipartite graphs; strongly regular graphs; ...
0
votes
2answers
47 views

Natural Deducion: assumptions can be used more than once?

Im trying to prove: $ \forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x)) \vdash \forall{x} \sim P(x,x)$ What i have: $\forall{x}\forall{y}(P(x,y)\rightarrow{}\sim P(y,x))\;$ Premise $ \forall{y}...
1
vote
1answer
47 views

What are the different ways to get a first-order formula that express the statement“$P$ is the $n$-th prime”

I know that such a $2$-predicate formula exists since Enderton's have already constructed such a formula in his text on mathematical logic but it was not easy to remember so I wonder if there is other ...
3
votes
1answer
80 views

Precise definition of Σ00 in the arithmetical hierarchy

I encountered several different definitions for Σ00 = Π00 = Δ00 of the arithmetical hierarchy. Following are two definitions which seem to me different but I'm not sure: All first-...
0
votes
0answers
15 views

First-Order Logic ternary predicate

I want to express the meaning of the following sentence in FOL: All the GermanAthlete are exactly those Persons who play a Sport for a Country where that Country is Germany. We have a ternary ...
1
vote
1answer
69 views

Arithmetical hierarchy: Why is $\Delta_0^0\ne \Delta_1^0$?

The definitions are different from one textbook to the other, but if we take the following definitions: $\Delta_0^0$ = all the first-order arithmetic formulas with bounded quantifiers only. $\...
1
vote
2answers
58 views

Expressibility of Peano arithmetic and the Arithmetical Hierarchy

First-order Peano arithmetic has no non-logical symbols other than S, +, *, < and variables. One allows finite quantification over predicates such as: $\forall k<n: \phi(k)$ where $\phi(k)$ is a ...
6
votes
2answers
62 views

Does the following set of formulas have a finite model?

So this is the problem: Do the following 3 formulas have a finite model: 1. $\forall x \forall y (p(x,y) \Rightarrow \neg p(y,x))$ 2. $\forall x \forall y (p(x,y) \Rightarrow \exists z (p(x,z) ...
0
votes
0answers
9 views

Source proof of equivalence between relation algebra and three variable first order logic

I am reading up on relation algebra and a lot about first order logic. Being a bit of a heavy torsion on the latter one as I am not used to it. Either way I read on wikipedia that up to 3 variable ...
1
vote
1answer
179 views

Optimize nonlinear model over time period (w/ Kuhn-Tucker Conditions)

I'm working on a nonlinear model that includes a time interval of 12 months. The goal is to maximize the total net benefit (NB) over the entire time period given the constraints listed below. I've ...
2
votes
1answer
22 views

Unification of $P(x,x)$ and $P(a,b)$ [closed]

Why can we not unify $P(x,x)$ and $P(a,b)$? Don't the substitutions $a/x$ and $b/x$ provide unification?
0
votes
1answer
24 views

Proving consequence by resolution refutation

I'm having trouble figuring out my error in this exercise: the task is to prove by resolution refutation that $ p \rightarrow (q \land r)$ is a consequence of the set $\{ p \rightarrow r, (p \land r)...
1
vote
0answers
24 views

What are some methods of proving undefinability results? (Reference)

I'm trying to prove some results regarding undefinability of functions from the natural numbers in certain structures, but besides texts on elemental logic and number theory, i haven't found anything ...
0
votes
2answers
43 views

Why is this counter-example valid?

I don't understand why the counter example of the following argument is valid: $\forall x\exists y(Ax\iff By)$ $\exists xBx \land \exists x\sim Bx $ $\forall x(Ax \to \sim Cx) $ ...
2
votes
1answer
27 views

Logical consequence problem

$P=(\forall x)(\exists y) GTOE(x,y)$ $Q=(\exists y)(\forall x) GTOE(x,y)$ And I want to know whether Q is an logical consequence of P. I know P is a logical consequence of Q. But I cannot identify ...
4
votes
1answer
86 views

what mathematical theorem is this

Reading Gödel, Escher, Bach by Douglas R. Hofstadter, at p. 552, Achilles asks the Crab to play this piece: ∀a:∃b:∃c:<~∃d:∃e:<(SSd * SSe) = b ν (SSd * SSe) = c> ^ (a+a)=(b+c)> And it seems ...
2
votes
0answers
39 views

Coloring (W-L Method)

I am trying to read An Optimal Lower Bound on the Number of Variables for Graph Identification. On page 3 (4th paragraph), it is written- It might color vertices and edges implicitly by using $k$-...
1
vote
2answers
38 views

Is there a finite set of sentences, $\Gamma$ which is satisfiable?

Prove/ Disprove: There's a finite satisfiable set of sentences above $\Sigma$ a monadic-language, $\Gamma$ such that $\Gamma $ is satisfiable only for structures with size larger than $5$. ...
0
votes
1answer
62 views

Difference of these two First Order Logic statements

1) $(\forall x)(\exists y)x{\le}y$ 2) $(\exists y)(\forall x)x{\le}y$ Assume that the domain of the variable is $D={0,1,2,...,99}$ These two statements says two things in natural language. I just ...
0
votes
1answer
25 views

$A,B$ satisfies on the same finite structures implies $A,B$ are logically equivalent?

$A,B$ are two sentences in Predicate Logic, such that for every finite structure $A$ is satisified iff $B$ is satisfied. Prove/ Disprove: $A$, $B$ are logically equivalent. I assume this ...
1
vote
1answer
42 views

Is this translation correct?

If I say some real numbers are rational it can be denoted in first order logic, $(\exists x)$ $(real(x) \land rational(x))$ Where $real(x)$ - x is a real number. $rational(x)$ - x is a rational ...
2
votes
1answer
23 views

Confussion about substitution use and free variables requirement for rules of inference in natural deduction

In our course of logic we've been given th following rules of inferences for introducing and eliminating quantifiers: $$ \frac{\Gamma \vdash \phi} {\Gamma \vdash \forall x\phi} \; x\not\in FV(\Gamma) ...
0
votes
1answer
39 views

Logical truth and logical consequence

I understand the concept of logical consequence, for example: 1.All persons are human 2.I am a person Conclusion: I am human. If 1 and 2 are true, conclusion must be true. My question is about <...
1
vote
1answer
23 views

first order structure and its usage

I am trying to wrap my head around "first order structure", What I've come up with so far is the following: First order structure is a non-empty set equiped with ...
1
vote
0answers
21 views

first order logic - help with translation algorithm between dictionaries

given a dictionary $\Sigma = \left \{f(),g(),R(,),c_0,c_1,c_2 \right \}$ and a sentence $\phi$ over $\Sigma$, I need to find an algorithm to translate $\phi$ to $\psi$ over $\Sigma'$ where $\Sigma' =...
0
votes
1answer
21 views

Logical Arithmetic: Distribution

Hi I'm reading through "How to Prove it" and I was doing one of the practice problems. The question asks you to simplify as far as possible and they give you the following: $$\neg(\neg p \vee q)\vee (...
0
votes
0answers
29 views

substitution lemmas for first order logic

How can i prove $ \text{$\models$}_{\Sigma} ((\forall x \ \varphi ) \ \Leftrightarrow \ (\forall y \ [\varphi]_{y}^{x}))$. Being $ \Sigma $ a signature, $ \varphi$ a formula, and $ [\varphi]_{y}^{...
0
votes
0answers
22 views

Prove or disprove a FOL sentence using relevant domain diagrams: $\exists x (a.x\to b.x) \to (\forall x\,\, ax \to \exists b.x)$

Prove or disprove the FOL sentence using relevant domain diagrams: $$\exists x (a.x\to b.x) \to (\forall x\,\, a.x \to \exists x\, b.x)$$ Can you suggest me a way to prove or disprove above two ...
0
votes
1answer
35 views

First order predicate logic for “Every bike is a two wheeler manufactured by Hero”.

Let $A(x)=x$ is a two wheeler $B(x)=x$ is a bike $C(x)=x$ is manufactured by hero. Which of the following is first order predicate logic for statement Every bike is a two wheeler manufactured ...
1
vote
0answers
33 views

Consistency Lemma in Lindenbaum's Theorem

Let $\Lambda$ be a modal logic, we say that a formula $\varphi$ is $\Lambda$-inconsistent if $\vdash_\Lambda (\neg \varphi)$ and is consistent otherwise. Similarly we say that a set of modal formulas $...
1
vote
0answers
29 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
72 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 ...
2
votes
0answers
69 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
19 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 x(P(x)...
2
votes
2answers
45 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
42 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: $\...