3 votes
Accepted

Prolog: Deletion of all appearances of an element in a list

There are some rules of thumb I follow when writing prolog. Two of them are: Use dif instead of \=. From the reference manual: &...
Alp's user avatar
  • 146
3 votes
Accepted

In predicate logic, is the "environment" only needed when free variables are present?

It is not so that the model alone allows you to make inferences and that you don't need an environment at all; it is rather that, if no free variables occur, then you may as well start with an empty ...
dkaeae's user avatar
  • 5,017
2 votes
Accepted

Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?

For any formula $\varphi$ in which $x$ and $y$ are free variables, $\forall x \> \forall y \> \varphi$ quantifies over all possible values for $x$ and $y$. As a result, $x$ and $y$ may be ...
dkaeae's user avatar
  • 5,017
2 votes
Accepted

Negation of the semantics of the Until operator in LTL

First, note that you did not really get the "first part the the expression correct". The first formula is, roughly, of the form $$ \forall i, (p(i) \lor q(i)) $$ while the second one is of the form $$...
chi's user avatar
  • 14.6k
2 votes
Accepted

How to correctly negate a predicate bounded by some quantifiers?

I'm not sure how general this type of problem is so I can't tell you if this will always be the best approach, but in this case you can move the negation to the top for more clarity. $$\forall x\ \...
integrator's user avatar
  • 1,110
2 votes
Accepted

Combining Predicate Logic and BigO

What the definition is saying is: $f\in O(g)$ if there's a number $n_0$ such that $f(n)$ is less than some multiple of $g(n)$ (that's where the $c$ comes in) for all $n$ larger than $n_0$. In simple ...
Rick Decker's user avatar
  • 14.8k
2 votes
Accepted

First-order logic - Does there exist a sentence that is satisfiable by all infinite models and only by them?

Probably the easiest way to prove this is using the compactness theorem: assume for contradiction that $\varphi$ is such a sentence. For every $n\in\mathbb N$, let $E_n$ denote the sentence $\exists ...
Emil Jeřábek's user avatar
1 vote
Accepted

Proving a predicate assignment is correct

What does it mean to have "suitable pairs of memory"? In the case of the Definition 3.8 it means exactly any pair that makes $(\sigma,\underline{\sigma})\vDash P(q_1)$ true. If it's not true ...
Alex Chichigin's user avatar
1 vote
Accepted

Domain of discourse vs First-order theory

Unless I'm missing something, you're simply asking a different question than the previous questioner did. The previous question is asking an abstract question about predicate logic, so all axioms are ...
Pseudonym's user avatar
  • 22.1k
1 vote

Complexity of pattern matching for modus ponens logical conclusions

This boils down to the question of whether there exists a polynomial-time algorithm for your matching operation. If there exists such an algorithm, call it $A$, then the answer to your question is yes:...
D.W.'s user avatar
  • 159k
1 vote

Encoding the theorem on friends and strangers in predicate logic

The first part doesn't ask you to prove anything. It just asks you to encode the theorem on friends and strangers in predicate logic. Let's build this statement step by step. First, we want to go over ...
Yuval Filmus's user avatar
1 vote

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

This is Exercise 83 in Schöning's book "Logic for Computer Scientists". Similarly, the solution to this problem can be found in the original paper of Robinson. He gives an example with ...
user1868607's user avatar
  • 2,194
1 vote

How to correctly negate a predicate bounded by some quantifiers?

F(x,y,t)⟹ person x can fool person y at time t. For the sake of simplicity propagate negation sign outward by applying De Morgan's law. ∀x∃y∃t(¬F(x,y,t))≡¬∃x∀y∀t(F(x,y,t)) [By applying De Morgan's ...
real albert einstien's user avatar
1 vote

In predicate logic, is the "environment" only needed when free variables are present?

The wikipedia article First-order logic calls the "environment" a variable assignment. A formula with no free variables is called a sentence. A model alone is sufficient to fully interpret a sentence. ...
Thomas Klimpel's user avatar
1 vote

Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?

For all means for all. If you want to say that "for all distinct $x$ and $y$ property $P$ holds", your formula needs to include a formula that enforces distinctness. $$\forall x\,\forall y\,(...
David Richerby's user avatar
1 vote

Predicate Logic - negating the conclusion to prove logical consequence?

The method works in the same way as proofs by contradiction. Suppose you have a set of assumptions $A$ and you want to prove that formula $\phi$ is a logical consequence of the formulas in $A$. One of ...
frabala's user avatar
  • 801
1 vote

Predicate Logics - double negation HELP me understand

The semantics of negation are very simple: $\lnot \alpha$ is True iff $\alpha$ is false. In your example, $\lnot (\lnot \forall x \lnot A(x))$ is True iff $\lnot \forall x \lnot A(x)$ is False iff ...
Yuval Filmus's user avatar
1 vote

Computability: Proving a predicate is not recursively enumerable

Show that your predicate is coRE-hard, that is, every coRE predicate reduces to it. If your predicate were RE, then it would follow that RE=coRE, which is known to be false. The rest of the answer ...
Yuval Filmus's user avatar
1 vote

Hoare triple: Loop invariant and correctness

I believe the loop invariant is the same as the postcondition, except with j and m swapped with i and n, respectively. That statement can be proven true at the start and end of each loop. This is true ...
Jeffrey L Whitledge's user avatar
1 vote

predicate logic proof of 2 numbers

As a hint, for any two numbers there is a third number in between.
Bjørn Kjos-Hanssen's user avatar
1 vote

predicate logic/binary relation help

This sounds like homework, and I do not wish to ruin the value of your homework for you by giving answers too quickly; the point of homework is to exercise and solidify the skills learned in the ...
Tom Zych's user avatar
  • 254
1 vote
Accepted

Discrete Mathematics Proofs for ∃ and ∀

Your solution is a good one, and that's how I'd prove it also. I don't believe a more straightforward or simpler version is possible.
Draconis's user avatar
  • 7,138

Only top scored, non community-wiki answers of a minimum length are eligible