40
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 ...
- 28k
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 ...
- 28k
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 ...
- 11.8k
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 ...
- 6,978
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 ...
- 261
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 ...
- 320
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."
- 80.1k
12
votes
Constructively deciding whether a decidable predicate holds universally
You are asking for a constructive proof of the Lesser limited principle of omniscience (LLPO), which states (in one of its forms) that for a decidable proposition $P$ on natural numbers
$$(\forall n \...
- 28k
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-...
- 269k
10
votes
Accepted
Can I use ellipses in first order logic
Strictly speaking, your statement is invalid because $\ldots$ is not part of the syntax of first-order logic. However, your statement is an abbreviation of a statement in first-order logic. For ...
- 269k
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 ...
- 24.9k
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 ...
- 28k
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 ...
- 29.1k
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 ...
- 28k
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: ...
- 24.9k
7
votes
Accepted
Solving SAT using tableau calculus
It can be, but the solution process is equivalent to converting a CNF formula to DNF, which is NP-hard. You will at worst end up exploring an exponential number of disjunction branches.
- 7,833
7
votes
Accepted
Horn clause to Prolog
A horn clause is a disjunction with at most one positive literal, e.g.
\begin{align}
\lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n \lor Y
\end{align}
The implication $X \rightarrow Y$ can be ...
- 808
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-...
- 28k
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 ...
- 269k
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 ...
- 11.8k
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.♦
- 140k
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 ...
- 2,445
6
votes
What is the point of (Compactness theorem in the) Overspill principle?
The theorem says that when a sentence has arbitrarily large (finite) models, then it also has infinite models.
The antecedent of the theorem:
$\phi$ is a sentence of predicate logic such that for ...
- 4,611
6
votes
Satisfiability of first-order logic is undecidable?
The fact that first-order logic (with some non-triviality constraints) is undecidable means that no algorithm can decide correctly whether a given first-order formula is true or not. However, for any ...
- 269k
6
votes
Accepted
Term rewriting; Compute critical pairs
Before adressing the actual questions, one remark on your work so far: the left cancellation in 2.a. is not correct in general, the critical pair would just be $x\circ(e\circ z) \approx x\circ z$. ...
- 2,138
6
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 ...
- 269k
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 ...
- 2,418
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 ...
- 269k
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 ~...
- 20k
Only top scored, non community-wiki answers of a minimum length are eligible