41 votes

Why is A implies B true if A is false and B is false?

Humans are bad at logic until they have to employ it to figure out human affairs. Think of "if $A$ then $B$" as a kind of promise: "I promise to you that if you do $A$ then I will do $B$". Such a ...
Andrej Bauer's user avatar
  • 30.4k
30 votes

Can proof by contradiction work without the law of excluded middle?

You asked (I am making your question a bit crisper): "What formal guarantee is there that it cannot happen that both $\lnot p$ and $p$ lead to a contradiction?" You seem to worry that if logic is ...
Andrej Bauer's user avatar
  • 30.4k
17 votes
Accepted

Why does soundness imply consistency?

I recommend looking into formal logic beyond vague, hand-wavy descriptions. It's interesting and highly relevant to computer science. Unfortunately, the terminology and narrow focus of even textbooks ...
Derek Elkins left SE's user avatar
17 votes

Why do ¬, ∀ and ∃ have the same precedence?

Order of precedence is simply a notional convenience. There is no notion of strength here, just notation. All three operators are unary operators with notation "$\circ\ \cdot$", where $\circ$ denotes ...
Discrete lizard's user avatar
  • 8,248
16 votes

Why is A implies B true if A is false and B is false?

It's a convention -- we could use a different one, but this one is convenient. Here's what Terence Tao says: This is discussed in Appendix A.2 of my book [Analysis 1]. The notion of implication ...
Hatshepsut's user avatar
16 votes
Accepted

How is ‘x + ½ = 2 and x ∈ ℤ’ an open statement?

$$x=1$$ $$∃x: x=1$$ The first is an open statement, since no value for $x$ is given. $x$ is called a free variable here. The second is a closed statement, because it talks about all possible values of ...
Stig Hemmer's user avatar
14 votes
Accepted

Predicate Logic Notation: What does a "dot" mean?

The dot just means "such that"; it's often omitted. The difference between the two formulas is the difference between "everybody has a mother" and "there is somebody who is everybody's mother."
David Richerby's user avatar
12 votes
Accepted

What is the relation between First Order Logic and First Order Theory?

First-order logic is a mathematical subject which defines many different concepts, such as first-order formula, first-order structure, first-order theory, and many more. One of these concepts is first-...
Yuval Filmus's user avatar
10 votes

Why is A implies B true if A is false and B is false?

"A implies B" means (short) "if A is true then B is true". It means (a bit longer) "if A is true then I claim that B is true; if A is false then I don't make any claim about B whatsoever". Now ...
gnasher729's user avatar
9 votes
Accepted

Algorithm for deciding alpha-equivalence of terms in languages with bindings

There are several ways to do what you want. One of them is to use a different syntax representation under which $\alpha$-equivalent terms are actually equal. Such representations go under the name ...
Andrej Bauer's user avatar
  • 30.4k
8 votes

Undecidable predicate logic is decidable by people?

The author is incorrect. A consequence of Godel's incompleteness is that any sufficiently complex logic has statements that are true, but have no proof of truth. If every statement had a proof or ...
Joey Eremondi's user avatar
8 votes
Accepted

How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over. Let us compare the situation to the definite integral, for concretness ...
Andrej Bauer's user avatar
  • 30.4k
8 votes

How is ‘x + ½ = 2 and x ∈ ℤ’ an open statement?

Whether it's an open statement or not depends on the structure of the statement, no on whether you can prove the truth value. Look at the second statement. There are three things you could substitute: ...
gnasher729's user avatar
7 votes

What is the relation between First Order Logic and First Order Theory?

The phrase "first-order logic" has two meanings: It is a chapter of mathematical logic in which we study certain kinds of formal systems and everything related to them. It is a special kind of first-...
Andrej Bauer's user avatar
  • 30.4k
7 votes
Accepted

Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic

Your argument shows that for each fixed $k$, the problem $k$-VC can be solved in polynomial time (indeed, the algorithm enumerates all sets of size $k$ and checks whether they are vertex covers, all ...
Yuval Filmus's user avatar
7 votes
Accepted

Any Non-trivial Logic System Defined with only Equality

If all you have is equalities and uninterpreted function symbols, then you have an algebraic theory a la universal algebra. A singleton set (or a collection of them in the multi-sorted case) is always ...
Derek Elkins left SE's user avatar
7 votes

Can proof by contradiction work without the law of excluded middle?

I think your question boils down to "when doing formal verification with some sort of formal logic, what sort of guarantee do I have that the logic is consistent?". And the answer is: none. That's ...
D.W.'s user avatar
  • 159k
7 votes
Accepted

Represent there are infinitely many in FOL

The existing answers provide examples of contexts where "there are infinitely many" can be expressed. However, there is an important sense in which "there are infinitely many" cannot be expressed in a ...
Noah Schweber's user avatar
6 votes

Why is A implies B true if A is false and B is false?

Let's take an example. Suppose that we want to express that $a$ is the only element of the set $S$ that satisfies property $P$. Then we can write $$ \forall x \in S \;\; P(x) \Rightarrow x = a $$ This ...
Yuval Filmus's user avatar
6 votes

How would one prove the pigeonhole principle with a SAT solver?

SAT solvers work in the propositional calculus, and usually accept as input a formula in conjunctive normal form. There are several different propositional variants of the pigeonhole principle; they ...
Yuval Filmus's user avatar
6 votes

Expressing 3-SAT in first-order logic

There has been a lot of work on formalizing mathematics, and in all of this work one needs to express definitions, theorems and proofs within the logic that one is using for formalization. This is ...
Hans Hüttel's user avatar
  • 2,496
6 votes
Accepted

What is the difference between $x:A$ and $x \Xi A$?

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~...
Dave Clarke's user avatar
  • 20.2k
6 votes
Accepted

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

Logic programming is proof search for some logic. Traditionally, this is the Horn clause fragment of first-order logic. Languages like lambdaProlog extend this to (intuitionistic) hereditary Harrop ...
Derek Elkins left SE's user avatar
6 votes
Accepted

Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though. Undecidability still holds for Curry-Howard: if ...
Joey Eremondi's user avatar
5 votes

What is the difference between superposition and paramodulation?

This is late for you, but probably might be of help to others. I myself had asked this question and I wrote the summary of my findings to the acl2-help mailing list on 8 and 9 September 2013: https://...
harshrc's user avatar
  • 51
5 votes
Accepted

Why is first-order logic (without arithmetic) VALIDITY only recursively enumerable, and not recursive?

However, I am not seeing why VALIDITY is not recursive as well, because given a formula $\phi$, one could run two Turing Machines for THEOREMHOOD, one on $\phi$ and the other on $\neg \phi$, ...
chi's user avatar
  • 14.6k
5 votes
Accepted

Using existential quantifier within implication

Your statement attempts to be express in formal logic the following sentence: There exist $\sigma_{opt}$ and $n$ in $R^+$ such that if $0 < n < 1$ then $\sigma_{opt} = n$. The attempt at ...
Yuval Filmus's user avatar
5 votes
Accepted

Undecidable predicate logic is decidable by people?

Keep in mind that the book was written for undergraduate students, and there are aspects of logic that will demand a considerable level of sophistication, which is often omitted at this introductory ...
André Souza Lemos's user avatar
5 votes
Accepted

Resolution of Barber paradox

No, you don't need to specially add any such clause. Here's where I think you might have gone wrong. The result is not 3 clauses (3 conjunctions). The result is a bunch of clauses. We get one ...
D.W.'s user avatar
  • 159k

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