Questions tagged [predicate-logic]
The predicate-logic tag has no usage guidance.
24
questions
1
vote
1
answer
122
views
Proving a predicate assignment is correct
I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification).
I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly.
I ...
user148883
1
vote
0
answers
24
views
Prove that any first-order logics with equality and a relation/functional symbol of arity more than 1 is undecidable
Definition: A formal logic system is decidable – if there is an algorithm that can determine if any given sentence is a theorem (or not).
Based on this definition, I am not sure how to move to prove ...
- 493
0
votes
0
answers
40
views
Why is “For all the simple things you have done to me, there exists one thing that makes me happy” FALSE? Use nested quantifiers to prove your point
I've done my due dilligence and tried to answer this question using every resource I could get. KhanAcademy, NesoAcademy, and Rosen's Discrete Mathematics book. I still can't wrap my head around it. ...
- 1
0
votes
1
answer
63
views
Domain of discourse vs First-order theory
In the question (Validity of predicate logic formulas) I see the following way of expressing:
"The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
- 113
1
vote
1
answer
74
views
First-order logic - Does there exist a sentence that is satisfiable by all infinite models and only by them?
Prove or Disprove: There is $\boldsymbol{no}$ alphabet $\Sigma$ and closed formula (no free variables) $\varphi$ above $\Sigma$,
such that for any Model $M$ it holds that
$M\models\varphi\iff\,|D^M|=\...
- 99
3
votes
1
answer
59
views
Complexity of pattern matching for modus ponens logical conclusions
Is a Turing machine with added the following contant-time operation equivalent (in the sense that polynomial time remains polynomial time and exponential time remains exponential time) to a (usual) ...
- 433
1
vote
1
answer
1k
views
Prolog: Deletion of all appearances of an element in a list
I am trying to create a predicate in Prolog which allows me to delete all occurrences of X in a list L. I have the following code:
...
-1
votes
2
answers
193
views
Encoding the theorem on friends and strangers in predicate logic
In every group chat of six (distinct) people on Instagram, there is a group of three (distinct) people such that either:
everyone in the group are friends
everyone in the group are strangers (i.e not ...
- 9
0
votes
0
answers
218
views
Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite
I'm kind of desperate at this point about this question.
A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a
sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
- 23
3
votes
1
answer
184
views
Combining Predicate Logic and BigO
I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
- 133
-2
votes
2
answers
121
views
How to correctly negate a predicate bounded by some quantifiers?
this is a problem which was asked in GATE CS 2010.
This is question statement:
Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
- 281
3
votes
2
answers
205
views
In predicate logic, is the "environment" only needed when free variables are present?
Suppose there exist no free variables in a given predicate logic formula. Is then a model alone sufficient to fully interpret the formula and make inferences? Don't we need an environment or variable ...
- 369
0
votes
1
answer
68
views
Predicate Logic - negating the conclusion to prove logical consequence?
In Predicate Logic, if you want to prove the logical consequence using the method of resolution, do you ALWAYS start off by negating the conclusion?
1
vote
1
answer
26
views
Predicate Logics - double negation HELP me understand
Sorry for maybe a silly question but i need to understand how
¬(¬∀x ¬A(x)) equals ∀x ¬A(x)
In my mind, the negation before the parenthesis will be applied to both ¬∀x and ¬A(x). So it would look like ...
2
votes
1
answer
126
views
Computability: Proving a predicate is not recursively enumerable
Let P(p) <=> for each x, comp(p,x) is defined.
Can anyone explain to me how to prove that P is not RE (recursively enumerable) ?
- 51
1
vote
0
answers
32
views
Natural deduction proof without any predicate
I am gaving trouble proving a natural deduction proof when there is no predicate given. Only conclusion is given. I understand the rules of elimnations, inclusions, IPs and others but I having trouble ...
- 11
0
votes
1
answer
241
views
Hoare triple: Loop invariant and correctness
The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving ...
- 21
2
votes
0
answers
158
views
Hoare triple: Loop invariant and partial correctness
Below there is Hoare triple in which variable $a$ is an array of integers, $len$, $x, i$ are integer-valued variables, and $r$ is a Boolean-valued variable. I have to provide a loop invariant (using ...
- 21
2
votes
2
answers
1k
views
Negation of the semantics of the Until operator in LTL
I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to:
$\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
- 23
1
vote
2
answers
79
views
Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?
Given the following predicate formula $F$:
$$\forall x \forall y [(\text{italian}(x) \Rightarrow (\text{winWC}(y) \Rightarrow \text{happy}(x))]$$
I am having trouble understanding whether $x$ and $y$...
- 262
0
votes
1
answer
73
views
What does it mean to logically imply another predicate?
Consider the following predicate formulas.
$F1: \forall x \exists y ( P(x) \to Q(y) ).$
$F2: \exists x \forall y ( P(x) \to Q(y) ).$
$F3: \forall x P(x) \to \exists y Q(y).$
$F4: \exists x P(x) \...
- 203
1
vote
1
answer
51
views
predicate logic proof of 2 numbers
For any two different numbers there is an number in between.
I'm trying to write this in predicate logic and have no idea how to do it, since I need 2 variables X and Y? For all x there exists a y ...
- 111
-1
votes
1
answer
145
views
predicate logic/binary relation help
(1) ∀x, y, z (x < y ∧ y < z → x < z) (transitivity)
(2) ∀x ¬(x < x) (antisymmetry)
(3) ∀x, y (x < y ∨ x = y ∨ y < x) (linearity)
I need to give an example of a (nonempty) ...
- 111
1
vote
1
answer
73
views
Discrete Mathematics Proofs for ∃ and ∀
Premises or Givens:
$∃x(A(x) → B(x))$
$∀x (B(x) → K(x))$
To Prove:
$∃x(A(x) → K(x))$
My Solution:
$A(z) → B(z)$ From premise and Existential instantiation $x$ for $z$
$B(z) → K(z)$ From ...
- 23