New answers tagged logic
2
A slightly weaker form of Gödel's first incompleteness theorem can be derived from the undecidability of the Halting problem with a short proof. The full incompleteness theorems also have a short proof which is similar to the one for undecidability of the Halting problem. I highly recommend the whole series (or at least the previous part) for context. The ...
2
Here $f$ is not a mathematical function. Rather, it is a function symbol. Don't think of $f(a,b)$ as the result of evaluating the function at parameters $a,b$. Rather, think of it as a term in a symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it.
If you like, you can think of it as ...
2
Because that's not how substitution is defined.
Seriously, there isn't much more to it than that. In some situations (such as applying a single step of a collection of rewriting rules), having the ability to substitute "each variable once, all at once" like this is important for the correctness of the definition. So substitution is defined so that there is ...
2
A unit clause of the form $p$ is the same as the clause $p \lor p$, and so corresponds to the arrow $\lnot p \to p$.
As an example, consider the unsatisfiable CNF
$$ p \land (\lnot p \lor q) \land \lnot q. $$
The implication graph contains the following edges:
$$
\lnot p \to p \\
p \to q,
\lnot q \to \lnot p \\
q \to \lnot q
$$
These can be arranged in a ...
1
By way of context, I'll assume the goal is to do unification in classical first-order logic in a fixed language $\mathscr{L}$. (Formatting and other corrections welcome.)
Briefly, you can treat arrays as terms and multidimensional arrays as arrays of arrays. You'll also introduce a new term symbol that doesn't occur in $\mathscr{L}$.
So for example, if you ...
0
You didn't say exactly what you tried, but it looks like you're trying to get there by applying elimination rules. That's not the simplest approach, and it might not work directly without case analysis on $P$ and $Q$ (I haven't tried). There's a very powerful theorem about natural deduction and most other basic logical framework: if there's a way to derive a ...
answered Mar 8 at 21:03
Gilles 'SO- stop being evil'
37.9k7 gold badges102 silver badges166 bronze badges
Top 50 recent answers are included
