# Tag Info

1

It depends a bit how you count / distinguish sets of sentences, If you assume that sets are closed under deduction then there is only one inconsistent set (the set of all sentences) all other sentences are consistent so the chance that you have the inconsistent set is almost nil. If you don't assume closure it is the opposite, every consistent set has ...

3

As you observe, $p\oplus q\oplus r$ is true when only one of the variables is true, or when all three are true. Therefore, $(p\oplus q\oplus r) \wedge \neg(p\wedge q\wedge r)$ would fit your needs.

3

The simplest formula is obviously, $$( p \land \lnot q\land \lnot r) \lor ( \lnot p \land \lnot q\land r) \lor ( \lnot p \land q\land \lnot r)$$ Maybe there is a more succinct and elegant formula but I can't seem to unearth it.

1

I'm able to prove it "independently" from the Deduction Theorem, but the proof is quite longer ... The axioms are : $F \rightarrow (G \rightarrow F)$ $(F \rightarrow (G \rightarrow H))\rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H))$ $(\neg G \rightarrow \neg F) \rightarrow ((\neg G \rightarrow F) \rightarrow G)$ For ...

3

For the non-trivial direction, you're given a model $B$ of the positive consequences of $\Gamma$ and you want an $A$ satisfying two requirements: (1) $A\subseteq B$ and (2) $A$ is a model of $\Gamma$. Notice that requirement (1) can also be phrased as "$A$ is a model of $\Delta$" for a suitable $\Delta$, namely the set of negations of all the sentence ...

3

Here's one way to do it (I think). Starting with $B$, we let $B'\subseteq B$ be a minimal model of the positive consequences of $\Gamma$. $B'$ can be obtained by transfinite recursion (taking intersections at limits). Now, we will show that $B'\vDash \Gamma$. Suppose not; that is, suppose $B'\vDash \neg \phi$ where $\phi$ is a consequence of $\Gamma$. It ...

-3

OTTER has found an 8 condensed detachment, level 5 proof: ----> UNIT CONFLICT at 11.16 sec ----> 26226 [binary,26225.1,2.1] $F. Length of proof is 8. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 2 [] -P(i(i(n(a),n(b)),i(b,a))). 3 [] P(i(x,i(y,x))). 4 [] P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). 5 [] ... 1 The proof must be : 1)$\lnot p \land \lnot q$--- premise 2)$\lnot p$--- form 1) by$\land$-elim 3)$\lnot q$--- form 1) by$\land$-elim 4)$p$--- assumed [a] 5)$\bot$--- from 2) and 4) by$\lnot$-elim 6)$q$--- from 3) and 5) by RAA (or Double negation) 7)$p \rightarrow q$--- from 4) and 6) by$\rightarrow$-intro, discharging [a] 8)$q$... 1 No, that is not correct. I'm assuming it's supposed to be some kind of natural deduction system, but the deductions you annotate with$\neg$elim and$\to$into don't follow any sane negation elimination or implication introduction rules I know. For example you try to conclude$p$from$\neg p$. That makes no logical sense "Socrates is mortal, ergo Socrates ... 3 I've found a related result into : Jon Barwise (editor), Handbook of mathematical logic (1999), A.2 : H.Jerome Keisler, Fundamentals of Model Theory, page 47-on. See page 72 : 5.10 : Lyndon Homomorphism Theorem (Lyndon [1959]). We can derive from the proof of it the application to the propositional case. Let$\Gamma$consistent, and let$\Gamma^+$the ... 0 There is an implied variable in this proposition, namely the day (or hour, etc.) being referred to. The question whether or not this is a tautology therefore does involve quantification over a domain which is potentially infinite, at least in some obvious formalisations. Therefore the question whether the proposition is a tautology is a bit more ... 1 Of course we can "speculate" on philosophy of language issues ad infinitum. BUT ... if we agree that propositional calculus can provide a very very simplified "model" of natural language, suitable for some limited applications, than we have to consider [see Dirk van Dalen, Logic and Structure (5th ed - 2013), page 5] : The linguistic entities occurring ... 0 The automated theorem prover OTTER has found a 10 step, level 5 proof: ----> UNIT CONFLICT at 4.26 sec ----> 11611 [binary,11610.1,2.1]$F. Length of proof is 10. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 2 [] -P(i(i(a,b),i(i(b,c),i(a,c)))). 3 [] P(i(x,i(y,x))). 4 [] ...

2

For me, this was one of the most difficult principles in predicate logic to apply, especially in longer proofs with many variables and sub-proofs. To establish the principle involved, I think it really helps to make the domain of quantification explicit for every quantifier as they do in mathematics. Consider the following examples. Example 1 Venturing ...

2

Both statements are not equivalent. As a rule of thumb, in such a sentence, the variables after the $\exists$ symbols depends on every variable declared before. Here, using this rule yields $$\exists y\ \ \forall x\ \ P(x,y)\\ \forall x\ \ \exists y(\color{red} x)\ \ P(x,y)$$ From here you see that there is no equivalence, but that the first implies the ...

2

They are different statements, in general. The second statement says that for every $x$ there is some $y$ such that $P(x,y)$ holds, while the first states that the same $y$ has $P(x,y)$ hold for every $x$. For example, say we consider the property $x \leq y$, talking about integers. Then $(\forall x)( \exists y)(x \leq y)$ is true - we can take $y = x$. But ...

4

We can formally prove that: $$\exists y \forall x P(x,y) \implies \forall x \exists y P(x,y)$$ but the reverse implication is not logically valid. Consider the $y$ promised by the first statement, a $y$ which satisfies $P(x,y)$ for every $x$. From this it may be seen that for every $x$, some $y$ exists such that $P(x,y)$. That is the informal ...

0

We have that : $∀xP(x,F_2) \Rightarrow ∃y∀xP(x,y)$ and : $∀xP(x,F_1(x)) \Rightarrow ∀x∃yP(x,y)$. See e.g Skolemization. In both cases the proof is straightforward : 1) $∀xP(x,F_2)$ --- assumed [a] 2) $\exists y \forall x P(x,y)$ --- from 1) by $\exists$-introduction 3) $∀xP(x,F_2) \rightarrow \exists y \forall x P(x,y)$ --- from 1) and ...

0

A number of tableau provers for modal logics at least can be found under http://www.cs.man.ac.uk/~schmidt/tools/ You might be interested in LotREC, Logics Workbench, Mettel (resp. its successor Mettel2) or the Tableau WorkBench. These are generic provers and can be used for many logics, but usually come with calculi for propositional logic (and others) ...

2


1


1

In your example, you don't start with "¬X∨Z∨¬Y". You start with the set of clauses which has as its members each conjunct of the the conjunction you've listed. If you check your other proofs you'll almost surely find that "¬X∨Z∨¬Y" does not appear anywhere in the proof. If it did, then you would have to have some way to cancel Z or equivalently, you ...

1

We can "dsitribute" the OR in $(A \vee B) \wedge (\neg A \wedge \neg C)$ to get $[A \wedge (\neg A \wedge \neg C)] \vee [B \wedge (\neg A \wedge \neg C)]$ One of the terms should seem supicious.

1

$(A \lor B) \land (\lnot A \land \lnot C) \longleftrightarrow (A \land \lnot A \land \lnot C) \lor (B \land \lnot A \land \lnot C) \longleftrightarrow False \lor (B \land \lnot A \land \lnot C) \longleftrightarrow B \land \lnot A \land \lnot C$

6

\begin{align} (A\lor B)\land (\lnot A \land \lnot C) & \equiv [(A\lor B) \land \lnot A] \land \lnot C \\ \\ & \equiv [\underbrace{(A\land \lnot A)}_{\text{False}}\lor (\lnot A \land B)] \land \lnot C \\ \\ & \equiv \lnot A \land B \land \lnot C \end{align} The first equivalence is simply due to the associativity of $\land$. The second is ...

1

See Resolution : The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If after applying a resolution rule the ...

1

We have : $$p → ( q → p) \equiv \lnot p \lor (\lnot q \lor p)$$ by Material Implication twice, $$\equiv (\lnot p \lor p) \lor \lnot q$$ by Commutativity and Associativity, $$\equiv (T \lor \lnot q) \equiv T$$ by Negation laws : $p \lor \lnot p \equiv T$ and Identity laws : $T \lor p \equiv T$, \equiv T \lor q \equiv (p \lor \lnot p) ...

0

$p\to q$ and $\sim p$ can be substituted with $1+p+pq$ respectively $1+p$, where $pq$ is short for $p\wedge q$ and $+$ is exclusive or. Therefore: $(p\to(q\to p))\equiv 1+p+p(q\to p)\equiv 1+p+p(1+q+qp)\equiv 1+p+p+pq+pqp\equiv 1$, since $r+r\equiv 0$ for all $r$. and $(\sim p\to(p\to q))\equiv ((1+p)\to(1+p+pq))\equiv 1 +(1+p)+(1+p)(1+p+pq)\equiv$ ...

0

Hint: $A\implies B$ is equivalent to $\neg(A\wedge\neg B)$ and also to $\neg A\vee B$. Use De Moivre and transform both formulas in a disjunction of conjunctions.

0

Just look at the possible truth values for (p,q) and check that the two formulas output the same value in the 4 cases. If you want an axiomatic proof you can do this: Since $a\to b$ is a notation for $\neg a\vee b$, we can unfold the first formula into $\neg p\vee (\neg q\vee p)$. This is actually equivalent to $true$, since $p\vee\neg p$ is always true. ...

Top 50 recent answers are included