Thoughts on natural deduction?
>Jupiter is a planet>Grass is green>If Jupiter is a planet then grass is greenThis is logic, folks. This is what the mathematicians are telling us is the correct description of reality. Yep. Ok.
>>16884507
>>16884499Somewhat less succinct than Hilbert systems, but somewhat closer to coding.I'll be honest and say that despite being deep in the formal logic and set theory trenches (I also had a category and a types phase), I never studied the sequent calculus to any sensible degree.
>>16884629Hilbert systems are retarded and have too many axioms.
I make lines, I add symbols to the lines.You cant explain that.
>>16884777>I make lines>I add symbols to the linesCorrect, you construct mathematical objects. Non-constructivist mathematics is retarded.
why are algebraicists x, y guys but logicians are p, q guys?
>>16884779No it isn't, watch this:2+2=4.
>>16884842
>>16884499basedeveryone should learn this, in order to have a clue about what mathematical reasoning is.
>>16884889>take 2 objects>place 2 more objects beside it>painstakingly count the 4 objects
>>16884894Could we design AI that reasons according that rules?
>>16884772lmao hilbert's system for propositional calculus literally has 3 axioms compared to 20 axioms in propositional sequent calculus LK
>>16884894>>16884919It's fun to do once you get the hang of it.
>>16884952Woops coulda just did this too but whatever lol both are perfectly validI like how I can just take an infinite number of premises and come to the conclusion I want tho lol. Logic is so weird.
>>16884919>>16884894>>16884952>>16884959Look guys XD
A tool with a comfy UI that I sometimes use ishttps://www.umsu.de/trees/#(%E2%88%80x%E2%88%83y(Fy%E2%86%92Gx))%E2%86%92(%E2%88%83y%E2%88%80x(Fy%E2%86%92Gx))
>>16884952>>16884959>DeM, 1If you're not careful you're gonna alert the constructivism goons here (DeM is equivalent to a weak form of excluded middle)
>>16884499Natural deduction is fine, but the way you write it is retarded. Just use goddamn λ-terms with variables instead of a linearized syntax with backreferences.
>>16884780P, Q are propositions and quopositions
>>16884985Wow I feel retarded hahaha
>>16884985You can derive DeMorgan's laws
>>16885038Your proof is fine in classical logic but wouldn't work in Constructivism because you can't do an indirect proof, double negation doesn't hold under Constructivist mathematics because it also relies on LEM.
>>16884906>take 2 objectsHidden assumption. Construct the number 2. >painstakingly count the 4 objectsYet another hidden assumption.
>>16885047what's the assumption?
>>16884499People who get too into any one formal deductive system are missing the forest for the trees.
>>16885109And you suggest
>>16885047>construct number 2Hidden assumption that this is necessary.
>>16884499What is the time complexity of recognizing an applicable rule of inference to use in a deduction?
>>16884919Yes they are called dependently typed proof assistants. Natural deduction is just a formalism of Aristotle's syllogisms.What you want though is causal AI where some model can do inductive reasoning on it's own and those are still primitive.
>>16885096>what's the assumption?That the number 4 exists and that you can pair items with it to count. Prove the number 4 and prove counting.
>>16887636Define the number 4 for me and I'll prove it exists
>>16887692One pair of two objects
