# Tag Info

0

you can prove that: (p∨q)∧(∼p∧q) => ∼p∧q < simplification > ∼p∧q => q => p∨q => (p∨q)∧(∼p∧q) < simplification > < addition > < conjunction > Therfore, (p∨q)∧(∼p∧q) <=> ∼p∧q

1

You can note that: $$p\lor q=(\lnot p\land q)\lor (p\land\lnot q)\lor (p\land q)$$ and: $$((\lnot p\land q)\lor (p\land\lnot q)\lor (p\land q)) \land (\lnot p\land q)=\lnot p\land q$$.

1

Write $X*Y$ for the connective described in the question. Suppose that there are only two inputs, $X$ and $Y$. Say that a gate with a certain outcome for each possible input is determinate. Then all determinate gates constructable out of $\neg$ and $*$ will either be functions of both $X$ and $Y$, or just $X$ or just $Y$, or neither. Say that a ...

2

Fitch-style notation is a particular approach to a more general method of proof, called natural deduction. One appealing feature of natural deduction is that it mirrors the structure of deductive argumentation. For example, an argument for a statement of the form "if $p$ then $q$" may begin with an assumption of the truth of $p$, followed by inferences ...

1

There is a subtle difference between the two: A proposition is a statement in either a natural or a formal language, for which it makes sense to ask whether it is either true or false. An assertion is a statement which one claims to be true. As such, assertions are more restrictive than propositions. For example: In a logic textbook, we read "It's ...

0

I use Polish notation and condensed detachment. axiom 1 CpCqp axiom 2 CCpCqrCCpqCpr axiom 3 CCNpNqCqp D1.3 4 CpCCNqNrCrq D2.4 5 CCpCNqNrCpCrq D5.1 6 CNpCpq

0

How about this: For every interpretation $\mathcal I$ (truth assignment to all atomics), consider the opposite interpretation $\mathcal I^o$ (negated truth assignment). Then $\phi^o$ is true under $\mathcal I^o$ iff $\phi$ is true under the $\mathcal I$ (here, structural induction goes through). As $\models$ means true under all interpretations, the result ...

0

We can use the Deduction Theorem : with it, we can easily get the "derived rule" of Syllogism : $A \to B, B \to C \vdash A \to C$. Now for the main proof : 1) $\lnot A \to (\lnot B \to \lnot A)$ --- Ax.1 2) $(\lnot B \to \lnot A) \to (A \to B)$ --- Ax.3 3) $\lnot A \to (A \to B)$ --- from 1) and 2) by Syllogism. We can get rid of the ...

1

Hint for a possible solution, using the Natural Deduction proof system. I'll make a couple of assumptions : (i) I'll assume the Natural Deduction proof system for classical logic; (ii) I'll assume the following definition of inconsistency; we say that $X$ is inconsistent iff : $X \vdash \bot$. Then, the given is : $X \cup \{ \lnot \alpha \} \vdash ... 1 As Peter Smith points out, the answer is no. However, there does exist a meta-theorem which allows for replacement with conditionals which allows for replacement of a sort depending on where the subformula you replace appears. For more details, see the following site and the referenced papers: http://home.utah.edu/~nahaj/logic/concepts/semi/index.html ... 3 Let$\bot$be your favourite contradiction, and let$B$be a propositional variable. Then$\vDash \bot \supset B$(a contradiction materially implies anything). But not$\vDash \neg\bot \supset \neg B$(a tautology doesn't fix that$B$is false!). So that gives a counterexample to your conjecture (with the context$C$being simply constructed by taking ... 3 There are 16 possible binary logic operators (that is, operators like ⋀ and ⋁ that return a true or false value based on two inputs). 4 of them depend on one value while completely ignoring the other, while 2 more (always true and always false) ignore both values. So only 10 of the operators are of any interest. These 10 have been given a variety of names, ... -2 How about: Define g:((A+(A->0)->0)->0 by g(f) = finr(finl) The type of functions A->0 is the negation of A and A+(A->0) is the type of A or not(A). The construction of g is the proof we want. inl:A -> A+(A->0) is the left inclusion. inr is the right inclusion. I hope it is clear now. The notation comes (to me) from the HoTT book. 2 $$x = -1 \implies x^4 = 1$$ $$x = -1 \implies x^3 = -1$$ But $$x^4 = 1\not\Rightarrow x^3 = -1$$ because$x^3$could be equals to$1. 2 \begin{align} \mathcal A & = \{5,6\} \\ \mathcal B & = \{1,2,3,4,5,6\} \\ \mathcal C & = \{3,4,5,6,7,8,9,10\} \\[12pt] A & = [x\in\mathcal A] \\ B & = [x\in\mathcal B] \\ C & = [x\in\mathcal C] \end{align} TheA\to B$and$A\to C$are true but$B\to Cis false. Second example: \begin{align} A & = [x\in\{1,2,3,4,\ldots\}] \\ B ... 0A$: "I do not exist"$B$: "I work for a living"$C$: "I am a billionaire" In other words, make$A$false,$B$true,$C$false. 0 You can see : Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990), Ch.3.3 Propositional Resolution, page 45-on for a complete treatment of the proof system based on the Resolution Rule. The proof system "expands" the set of cluases, applying the Resoultion Rule in order to add e new clause (a disjunction) to the original set of ... 1 We'll ignore the inappropriate "Warning 2" in a charitable way .... Assume a subformula is a segment of a formula which is itself a formula. Let$X_1, X_2, \ldots X_n$be a formation chain for$\alpha$, and let$\beta$be a subformula of$\alpha$. Let$X_b$be the first member of the chain that has$\beta$as a subformula. There must be a first such ... 1 Every step almost ends up as correct up to a point. The last line needs to have the same scope as the set of premises {1, 2, 3}. That is the only incorrect step. Yes, you can use the outer assumption towards negating your inner assumption. Natural deduction systems assume a rule of repetition which allow you to repeat any assumption from an outer domain ... 0 From ~ A → (S ∧ R), ~(S ∧ R) → A or ((~S)$\lor$(~R)) → A. But we are given ~R. Therefore A. 1 We want to be able to make typing judgments like$\vdash \lambda x\cdot x : \sigma \to \sigma$. And to do this we have to use the rules and nothing else to construct a formal derivation of this typing judgment. In this example, the derivation looks like this: $$\begin{array}{c} x : \sigma \in \{x : \sigma\}\\\hline x : \sigma \vdash x : \sigma\\\hline ... 0 Your understanding is correct, but it may help to address a few other things you seem to be dealing with. Here is your problem as it currently stands: Problem: Suppose P \to (Q \to R). Prove that \lnot R \to (P \to \lnot Q) using truth tables. It may be helpful to rephrase this symbolically; you are being asked to show that the following ... 0 You can always use truth tables of both logical statements because it is only four combinations of truth - > (T,T) (T,F) (F,T) and (F F). 1 Define A\Delta B=(A\cup B)\setminus (A\cap B). Write out the LHS explicitly:$$(A\Delta B) \cup C = (A\cup C) \Delta (B\setminus C)=((A\cup B)\setminus (A\cap B))\cup C=(A\cup B \cup C)\setminus (A\cap B)$$Write out the RHS explicitly:$$(A\cup C) \Delta (B\setminus C)=((A\cup C) \cup (B\setminus C))\setminus((A\cup C) \cap (B\setminus C))=(A ... 2 $$(A \Delta B )\cup C = (A \setminus B) \cup (B \setminus A) \cup C = (A \setminus B) \cup C \cup [(B \setminus A) \setminus C]$$ $$= [(A \cup C) \setminus (B \setminus C)] \cup [(B \setminus C) \setminus (A \cup C)] = (A \cup C) \Delta (B \setminus C).$$ Comment if you want to have the steps more explained in detail 0 You just need the usual properties of the connectives and double negation elimination. I suggest you to try a proof of it to make clear the chain of reasoning you need. Using the natural deduction method: 1)$\neg(A \wedge B)$, Premise$\quad$2)$\neg(\neg A \lor \neg B)$, Assumption$\quad \quad$3)$\neg A $, Assumption$\quad \quad$4)$\neg A ...

2

The "system" $\mathsf {TNT}$ of Typographical Number Theory is "nothing special"; we can have several different Formal systems : what counts is their "expressive capability". Propositional calculus has a very limited expressive capability, but it is very useful for pedagogical reason, because with it it is possible to show the basic concept and properties ...

Top 50 recent answers are included