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

Questions tagged [predicate-logic]

Questions concerning predicate calculus, i.e. the logic of quantifiers.

0
votes
1answer
26 views

Translating set syntax in FOL

Even though the formal syntax rules for first order logic talk about $\forall x$ or $\exists x$ without necessarily including any kind of $\in Y$ part for some domain/set $Y$, sometimes we'll see ...
3
votes
1answer
56 views

Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

I am interested in how one would formally prove: $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$ I realize that it's basically saying that: $\lnot(P(x_0) \land P(x_1) \land ... \land P(x_n)) \...
1
vote
1answer
38 views

Substitution Theorem on “A Concise Introduction to Mathematical Logic” by W. Rautenberg

I'm trying to understand the Substitution Theorem (Theorem 3.5, page 71) in "A Concise Introduction to Mathematical Logic" by W. Rautenberg. At some point Rautenberg states: "The reader should recall ...
0
votes
1answer
22 views

Does each variable in a premises undergoing Universal Instantiation have to change?

I'm currently working on this problem: “All movies produced by John Sayles are wonderful. John Sayles produced a movie about coal miners. Therefore, there is a wonderful movie about coal miners.” ...
0
votes
0answers
19 views

Symbols of the language vs. Free variables

For some context: I'm currently taking a course of Formal Methods and Logics and there's a passage where we show that the monadic second order ($\text{MSO}$) theory of (possibily labelled) linear ...
1
vote
1answer
22 views

Divisibility represented by Boolean logic

Some context: I was thinking about the feasibility of using SAT solvers to prove primality, especially of Mersenne primes, by showing that there exists no Boolean sequence $d_1,d_2, ..., d_{b'}$ that ...
3
votes
4answers
59 views

Proving logical equivalences in the statements $(∃𝑥)(𝑃(𝑥) → 𝑄(𝑥))$ and $(∀𝑥)𝑃(𝑥) → (∃𝑥)𝑄(𝑥)$

For this I must show that the two statements $(∃𝑥)(𝑃(𝑥) → 𝑄(𝑥))$ and $(∀𝑥)𝑃(𝑥) → (∃𝑥)𝑄(𝑥)$ are logically equivalent. The issue I'm coming up with is that I'm unsure about the proper methods ...
1
vote
3answers
45 views

Difference between $(\forall x A(x)) \implies (\forall x M(x))$ and $\forall x (A(x) \implies M(x))$

I don't understand the difference between $$(\forall x A(x)) \implies (\forall x M(x))$$ and $$\forall x (A(x) \implies M(x))$$ How do the additional quantifiers change the statement?
0
votes
1answer
15 views

First order logic from computational linguistics - implication

I am reading Natural Language Understanding by James Allen. It has the following sentence That John is rich implies that he is happy. And first order logic ...
0
votes
1answer
43 views

How to prove two statements are equivalent and give a counterexample if they're not.

I'm trying to solve this question. Let A be a set and P(x) and Q(x) be statements with one variable Are the statements $$((∃x ∈ A)(P(x)))∨((∃x ∈ A)(Q(x)))$$ and$$(∃x ∈ A)(P(x)∨Q(x))$$ ...
0
votes
1answer
30 views

Understanding definable set

I'm facing some difficulties in understanding what its mean to prove that a set is a definable set. Below is an example of a question that was given in our class, with the solution for this question. ...
0
votes
1answer
43 views

Metalanguage of mathematics

What excactly is the matalanguage of mathematics? I mean, the predicate calculus admits the formal language of mathematics, right? Then we add set axioms to it et voilá: mathematics. But what does ...
0
votes
1answer
32 views

A 7-formula deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$. Enderton logic page 123.

Enderton claims that it is not hard to show that a deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$ exists, and furthermore that it consists of only seven formulas. I was able to ...
-1
votes
0answers
18 views

isomorphism classes/number of models up to iso

What does it mean here on the page $73$ the second $\aleph_2$ in $\dot{I}(\aleph_2,\aleph_2)$ ?
0
votes
1answer
28 views

Nested Quantifier Practice Question: Some student has never been asked a question by a faculty member.

So I was practicing nested quantifiers for class, and I came to an answer which I think is right, but the book gave something slightly different. For starters, the context of the question is this: ...
1
vote
1answer
41 views

Translation of sentence into predicate logic. “Greeks who fear Romans, fear only romans.”.

I am trying to figure out how to translate this sentence into predicate logic: "Greeks who fear Romans, fear only Romans". R_ _ : _ Fear _ x: Greeks y: Romans z: Others This is my crack at it, ...
1
vote
1answer
21 views

How to solve ∃x:X.PvQ |- (∃x:X.P) v (∃x:X.Q)?

What I've done is the following however I'm stuck on PvQ ...
0
votes
1answer
103 views

Free variables in set-builder notation and equational definitions. [closed]

I have a problem in understanding quantification for set-builder notation (comprehensions) and equational definitions. For example, $odd$ natural numbers can expressed as: $\{ x \in \Bbb N \mid \...
0
votes
2answers
38 views

Negation of Quantified Statements

I was wondering if someone could walk me through how to do this type of question, my teacher didn't really explain it well enough for me to follow along. QUESTION: Let D = E = {−3, 0, 3, 7}. Write ...
0
votes
0answers
25 views

Unsatisfiable Union but parts can be satisfied by P and not P

Suppose that G1 and G2 are theories and that G1 Union G2 is unsatisfiable. Prove that there is a sentence P s.t. every model of G1 satisfies P and every model of G2 satisfies not P. I do not entirely ...
-1
votes
0answers
18 views

Prove that $\exists x:X\cdot(P\implies Q)\vdash(\exists x:X\cdot P)\implies (\exists x:X\cdot Q)$

I am tring to work out this question regarding predicate logic. $(\text{a})$ Formally prove that: $$\exists x:X\cdot(P\implies Q)\vdash(\exists x:X\cdot P)\implies (\exists x:X\cdot Q)$$ I have ...
1
vote
1answer
28 views

Is my way of interpreting a model correct?

A model $M$ is a tuple $(O, F, P)$, where $O$ is a list of objects, $F$ is a table of function values, and $P$ is a table of predicate values. Let $O=\mathbb{Z_{\le4}}$. I use $even(x), prime(x)$ ...
0
votes
1answer
36 views

Atom in first order programming

Consider the following statements regarding atom in first order programming An atom is a predicate applied to a tuple of objects. Atoms: An atom evaluates to a number. A scalar, a ...
1
vote
2answers
39 views

What is the difference between value and constant literal in first order logic syntax?

In FOL, there are two values true and false; In FOL, there are two constant literals : T and F; Is there any difference between the both (values and constant literals)? Can I say that true value is ...
0
votes
0answers
29 views

Translate the following sentence into a predicate formula:

There is a student who has e-mailed at most n other people in the class, besides possibly himself. The domain of discourse should be the set of students in the class; in addition, the only predicates ...
0
votes
4answers
70 views

Understanding sorts in many sorted logic intuitively

I have a variable set $v$ of size 6. $V =\{a,b,c,p,q,r\}$ I have two statements $\forall_{x \in \{a,b,c\}} x$ is an integer $\forall_{x \in \{p,q,r\}} x$ is an irrational number Now I am using a ...
-2
votes
1answer
55 views

Logic and uniqueness

How do you prove statements of the following forms? 1) $\forall x\in X: \exists ! Q(x)$ 2) $\exists!x \in X: \forall P(x)$ For instance, if I wanted to show that $\exists! x\in \mathbb{N}$ such ...
0
votes
1answer
36 views

Function symbols in many sorted logic

Consider the following definition We fix an enumerable set Fun of function symbols. Each function symbol has associated to it an arity of the form $σ1 \times \...
0
votes
1answer
44 views

Did I translate this correctly?

Consider the proposition: “If someone in your class has a dog, then everyone in your class has a cat.” -Translate this sentence into mathematics, letting D(x) be the predicate “x has a dog”, C(x) ...
0
votes
2answers
48 views

How to prove this logical equivalence in predicate logic?

Prove that: $ ( \forall x)(\forall y)(\exists z)((P(x)\Rightarrow Q(y)) \wedge \neg Q(z))$ is equivalent with $ \neg((\exists xP(x) \lor \forall zQ(z))$ How should I attempt such problems? I tried ...
1
vote
2answers
77 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
0
votes
1answer
34 views

Proving certain obvious tautologies in the calculus of constructions

I'm trying to prove that $\lnot (\exists y : S.Py) \rightarrow \exists y : S. \lnot Py$ (let me know if the encoding of $\exists$ matters!). I don't have any good ideas about how to do that, but I've ...
0
votes
0answers
24 views

Are there any proof assistants based on logic programming?

Logic programming is a programming language paradigm. In it, a programmer creates a bunch of axioms in the form of horn clauses, representing computations, which the implementation of the language ...
0
votes
1answer
133 views

Find the argument form for the argument and determine whether it is valid

I have been trying this question for about 3 hours and I am still stuck please help. Q: Find the argument form for the argument and determine whether it is valid. Explain your reasoning. If I get a ...
0
votes
1answer
20 views

Formal proof method for predicate logics

I am looking for the official name for a proof method, The method consists of proving the INconsistency of a theory. This was done using trees. We call it classic-elimination method but I don't know ...
0
votes
1answer
23 views

Prove that structure M is not Herbrand structure

I've been trying to solve the following problem, but I get a bit confused with the solution I get. Here's the problem: Let's M be a structure with an universe all the terms with no variables. We know ...
0
votes
0answers
24 views

Greatest common divisor in predicate logic with one binary functional symbol

Lets have one binary functional symbol $f$, where $f(x,y)=xy$. Show that in the universe of $\mathbb{Z}$ every two numbers have Greatest common divisor. So far my solution look like this: $$\exists ...
1
vote
2answers
87 views

Translate this sentence to predicate logic

The question given asks to translate to predicate logic: Every positive real number has a unique positive real root. My solution to this problem is to separate it into the appropriate quantifiers. ...
1
vote
2answers
43 views

First-order formulas with exponentially large models

The separated fragment of First-Order Logic (FOL) is the sublanguage of FOL in which no atomic sub-formula $A(\ldots,x,\ldots,y,\ldots)$ is such that $x$ is bound by and existential quantifier and $y$ ...
1
vote
1answer
32 views

Prove that the class of dense linear orders cannot be axiomatized by purely universal sentenes [closed]

That is, prove that there is no set $T$ of purely universal sentences such that for every structure $A$ over the signature $\{\leq\}$, $A$ is a dense linear order iff $A\models T$.
0
votes
0answers
8 views

First order natural deduction proof [duplicate]

I have been stuck with a natural deduction proof of a first-order logic theorem, which has already been discussed here Tricky proof in Natural Deduction [¬∀x∃y¬Rxy ⊢ ∃x∀yRxy]-help ...
0
votes
1answer
41 views

formalize in predicate logic: All students join some course that they don't like.

I came up with two formulas and have no Idea whether their correct. 1. ∀x(S(x)∧¬C(x)) 2. ∀x∃y(S(x)∧C(y)→DoesNotLike(x,y)) And then I have one a bit more complicated, that I can think of multiple ways ...
0
votes
1answer
35 views

Easy example of a herbrand structure

Can someone give me an easy example of a Herbrand structure? I can't really visualise the difference between a Herbrand and a normal structure.
0
votes
2answers
26 views

∀x(I(x) → ∃y(I(y) ∧ (x < y))), I(x): x is an integer

∀x(I(x) → ∃y(I(y) ∧ (x < y))), I(x): x is an integer Is the following a correct translation? For all x, if x is an integer, then there exists an y such that y is an integer and x < y. Is this ...
1
vote
1answer
46 views

How to read $\exists x \forall y \exists z((x + y)z = 1)$?

$$\exists x \forall y \exists z((x + y)z = 1)$$ How can I translate this expression to English? And is the statement true or false? (for numbers in $\Bbb R$). $z=1$ is the part that confuses me.
0
votes
0answers
37 views

Galois types as equivalence classes

In the context of Galois types let $p=(M,a,M')/\sim$ for some $a$ and for some $M'\succeq M$, with $a\in M'$ Since $M$ is an amalgamation base and $M'\succeq M$ and $N\succeq M$ there is some $N'$ ...
2
votes
1answer
37 views

Definition of a structure

I found the following definition for a structure in my math course: A structure $X$ consists of a non-empty set $D_x$, the universum of $X$ and the attribution of values $r^x$ to non logical-symbols $...
0
votes
0answers
13 views

Logical connectives [duplicate]

I need help with the below question to write the logical connectives statement.
0
votes
1answer
24 views

how do express “multiple” in predicate logic?

I hope you can give me some tips on how to translate part of the following sentence into predicate logic: “No woman loves a man that loves multiple women”. Which quantifier would you use to express ...
0
votes
2answers
38 views

States that reach only bad states are bad. Predicate Logic

Consider a system of states with a binary relation R. If R(x,y) holds, we say that state x reaches state y. Further, consider two unary predicates I and B where I(x) means that x is an initial state ...