39
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 promise says nothing about what I might do if you fail to do $A$. In fact, I might do $B$ anyhow, and that would not make me a liar.
For instance, suppose your ...
30
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 inconsistent, then proof by contradiction is problematic. But this is not the case at all.
If logic is inconsistent then proof by contradiction is still very much ...
17
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 the operator symbol $\exists, \forall,\neg$ and $\cdot$ the operand. There can never be any ambiguity in which order to apply these operators: the operator to ...
16
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 used in mathematics is that of material implication, which
in particular assigns a true value to any vacuous implication. One
could of course use a different ...
16
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 specifically about formal logic can present a warped picture of what logic is. The issue is that most of the time when mathematicians talk about "logic", they (...
15
The answer is really in the first paragraph of the quoted text, so what I'm about to attempt is really a rephrasing of that.
Remember that $\Gamma \vdash \psi$ means that there exists a formal proof of $\psi$ (in the system from $\Gamma$ blah blah blah). That is, there's some way, starting from the axioms, to syntactically manipulate the symbols according ...
13
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."
12
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 \in \mathbb{N} \,.\, P(n)) \lor \lnot \forall n \in \mathbb{N} \,.\, P(n).$$
That's exactly your problem. It is well known that LLPO is not provable ...
12
Logic with unary predicates (not operators), is called monadic. The thing that is called propositional logic only has nullary predicates, i.e., constants true and false, and no quantifiers.
The undecidability of predicate logic follows because predicate logic (with at least one binary predicate) is powerful enough to describe how a Turing machine works, and ...
12
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-order theory: it is a set of first-order formulas. Often we consider the first-order theory generated by a finite number of axioms and axiom schemes. Such a ...
11
I'll start with your last question (in the comments); namely "Why doesn't x = y satisfy the initial problem".
The answer is in the quantifiers. Read from left to right. It starts with "there exists" X. So pick an X in your head. Say X = 5. We can not pick Y here because it doesn't have a value yet and we MUST pick a value for X NOW. Now proceed to read the ...
11
Resolution is complete as a refutation system. That is, if $S$ is a contradictory set of clauses, then resolution can refute $S$, i.e. $S \vdash \bot$.
This is sufficient since $T \vdash A$ is equivalent to $T \cup \{\lnot A\} \vdash \bot$. So if we want to see a formula $A$ is derivable from $T$, we only need to check if there is a refutation proof for $T \...
10
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 example, when $n = 3$, your statement is an abbreviation of the bona fide statement
$$ \forall x, \exists y_1, y_2 (x \neq y_1) \land (x \neq y_2). $$
As long as you ...
10
"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 take "If the sun is green then the grass is green".
In the long form it is translated to "If the sun is green then I claim that the grass is green; if the sun is ...
9
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 nameless or locally nameless syntax. A popular one uses de Bruijn indices. See my blog posts How to implement dependent type theory I, II and III for a blitz ...
8
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 written as disjunction $\lnot X \lor Y$ (proof by truth table). If $X = \lnot X_1 \lor \lnot X_2 \lor \ldots \lor \lnot X_n $, then $\lnot X$ is equivalent to $...
8
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 disproof, then we could iterate through all strings, check if it was a proof or disproof, and eventually we'd find one, making logic decidable. We know that this ...
8
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 something you have to assume. Formal verification doesn't eliminate all assumptions; it just helps you be clearer about what you are assuming, and maybe helps ...
7
Short answer. There is no such first-order formula, you need a monadic second order formula.
Details. This can be proved directly using an Ehrenfeucht-FraÏssé games argument if you want to stay inside logic, but the real answer to your question is the conjunction of three results.
[1] Büchi (1960): A language is monadic second order expressible iff it is ...
7
In §3.2 they distinguish between the following four grammatical categories, with some examples:
Predicates: Woman, Rich, Beautiful, Bankrupt
Relations: LivesAt, HadAnAffairWith, Loves
Functions: fatherOf, bestFriendOf, ceoOf
Individual constants: maryJones, johnQSmith, tomsHouse
In the background they have first-order logic with identity, which means ...
7
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
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-order theory, namely the one generated by an empty signature and an empty set of axioms.
Your question refers to the second meaning, but to understand this, we ...
7
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 a model of an algebraic theory. That is, every algebraic theory is, at least, trivially satisfiable. So if both $S$ and $F$ are required to simply be ...
7
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 first-order way without some additional context restrictions:
Specifically, fix your favorite first-order language $\Sigma$. Then it's a consequence of the ...
6
You could start by considering simplified versions of the rules and build intuition by considering those cases. For instance,
$$\frac{\neg A, \ B \implies C}{B \implies C, \ A} (\neg L)$$
can be interpreted as stating that $(\neg A\wedge B)\Rightarrow C$ implies
$B\Rightarrow (C\vee A)$.
So if it is the case that $\neg A$ and $B$ are true implies $C$ ...
6
It is false if and only if there is a number that is equal to zero.
"There is a number that is equal to zero" is true if and only if zero is a number. Without any context (there might e.g. be some very strange definitions given earlier in the exercise), we cannot say whether zero is considered a number in this case. If there is no other context given in the ...
6
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 any natural
number $n \geq 1$, there is a model of $\phi$ with at least $n$
elements.
is equivalent to saying that there are infinitely many different ...
6
Resolution is only refutationally complete, as you mentioned. This is intended and very useful, because it drastically reduces the search space. Instead of having to eventually derive every possible consequence (to find a proof of some conjecture), resolution is only trying to derive the empty clause.
6
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 translation goes about by replacing English words by mathematical symbols, while keeping English syntax. Unfortunately, that is not how this sort of translation ...
Only top voted, non community-wiki answers of a minimum length are eligible
