4,236 reputation
1027
bio website
location
age
visits member for 3 years, 2 months
seen 1 hour ago

Jul
22
answered Where's the problem with a false “proof”: $\;1^0 = 1^2 \overset{?}\implies 0 = 2$
Jul
22
comment Where's the problem with a false “proof”: $\;1^0 = 1^2 \overset{?}\implies 0 = 2$
I'm not so sure. What if the argument was that the conjunction of "$$\large 1^1=1^2$$ and $$\large 0^1=0^2$$ is true, therefore 1=2?
Jul
22
comment Is this a valid natural deduction?
On the other hand this does show that if one considers a system with the rules used in the proof analysis of the OP's proof, that left-disjunction introduction becomes a derivable rule of inference. One might argue that it should be a derivable rule of inference, since from just conditional introduction and conditional elimination we have p $\vdash$ CCpqq, and since the truth table for CCpqq and Apq match, we can think of this as implying that left-disjunction introduction is a valid rule of inference.
Jul
21
comment The (un)decidability of Robinson-Arithmetic-without-Multiplication?
Oops! Sorry, I misread your question.
Jul
21
comment What does “calculus” mean?
A calculus consists of a means of computing formulas.
Jul
21
comment The (un)decidability of Robinson-Arithmetic-without-Multiplication?
The Wikipedia says this en.wikipedia.org/wiki/Robinson_arithmetic "The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which Gödel numbering forms a part). The axioms of Q [Robinson arithmetic] were chosen specifically to ensure they are strong enough for this purpose. Thus the usual proof of the first incompleteness theorem can be used to show that Q is incomplete and undecidable."
Jul
21
comment The (un)decidability of Robinson-Arithmetic-without-Multiplication?
"Since this cut down theory doesn't even know that addition is commutative..." I think you've given an interpretation to the operation "+" which the formal system doesn't have.
Jul
21
comment Are variables logical or non-logical symbols in a logic system?
logical........
Jul
20
comment Simplifying a categorical proof of constructive dilemma
@JoshuaTaylor Sorry, I haven't done much with term-weighting. I thought I might use the steps of your original proof as weight templates, but I'm not sure exactly what they are. Also, if we already have a proof with steps (a$_1$, ..., a$_n$), then one method of finding a shorter proof that I read in Larry Wos's notebooks consists in doing n runs. The first run has all of the steps (a$_2$, ..., a$_n$) weighted low (a$_1$ might need weighted high), the second run has (a$_1$, a$_3$, ..., a$_n$) weighted low, the third run has (a$_1$, a$_2$, a$_4$, ..., a$_n$) weighted low and so on.
Jul
20
comment How to prove theorems using axioms and lemmas
@user46944 There's often dozens upon dozens ways to prove a given theorem in a propositional calculus. If you eliminate redundancy, there's still usually quite a few different proofs that exist.
Jul
20
revised How to prove theorems using axioms and lemmas
added link to the textbook
Jul
20
comment How to prove theorems using axioms and lemmas
Here's an answer in Polish notation using condensed detachment. I gleaned this from Prover9, which ran for less than a second. 3 CxCyx 4 CCxCyzCCxyCxz 5 CCNxNyCCNxyx D3.3 7 CxCyCzy D4.4 8 CCCxCyzCxyCCxCyzCxz D3.4 9 CxCCyCzuCCyzCyu D4.5 11 CCNxNyCNxyCCNxNyx D3.5 12 CxCCNyNzCCNyzy D3.7 13 CxCyCzCuz DD4.3.3 14 Cxx D3.14 15 CxCyy D11.15 16 CCNxNNxx D3.16 17 CxCCNyNNyy D8.13 18 CCxCCyCzyuCxu D8.12 19 CCCNxNyCCCNxyxzCCNxNyz D8.7 20 CCxCCyxzCxz D20.17 21 CNNxx D20.9 22 CCxyCCzxCzy D5.21 24 CCNNNxxNNx D18.22 25 CCCxyzCyz D3.25 26 CxCCCyzuCyz D25.24 27 CxNNx D19.26 29 CCNxNyCyx
Jul
20
answered Expanding nested brackets
Jul
16
comment Is it always a tautology?
@YounisShah There do exist many-valued systems which have the same tautologies as bivalent systems. See the Bergmann book and the section on Bochvar's 3-valued systems for an example. Though, there probably is a greater amount of many-valued systems which have different tautologies than bivalent systems.
Jul
16
comment Is it always a tautology?
@YounisShah That is true, yes.
Jul
16
comment Is it always a tautology?
@YounisShah Goblin is correct. If the semantics are bivalent (or equivalently classical), then the answer to your question is an emphatic "yes". One might consult Merrie Bergmann's book "An Introduction to Many-Valued and Fuzzy Logic" and its references for more on non-classical systems.
Jul
16
comment Is it always a tautology?
The truth value of an equivalence V(p↔q) is equal to V(p)↔V(q). So, given that the diagonal of the truth table always evaluates to the designated value, then the equivalence here will hold. And since the semantics are still two-valued for the subsystem I've described, we have that the diagonal of the truth-table evaluates to the designated value "truth", and thus the equivalence holds.
Jul
16
comment Is it always a tautology?
@Goblin To start one's study, one could join any known axiom set for the implicational calculus of propositions to any known axiom set for the equivalential calculus under suitable rules of detachment and uniform substitution... such as the pair {CCCpqrCCrpCsp, EEpqEErqEpr} under the rules {C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$, {E$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$ with uniform substitution for variables. The equivalence will still hold, since the intended semantics are bivalent. If the truth value "V" of two propositions is equivalent, then V(p)=V(q). Now...
Jul
16
answered Is it always a tautology?
Jul
16
comment Is it always a tautology?
The deduction theorem doesn't require that a $\land$ connective exist. This proof isn't valid for the subsystem of propositional calculus which only has $\rightarrow$ and ↔ as connectives.