[04091948]

> If we can start from an assumption and perform a series of logical deductions and reach True, then we know our original assumption is True, that it is provable

is this a difference between mathematical and natural language?

my understanding is if you deduce something true from an assumption it means nothing.

you need to deduce something false and thus the negation of your assumption is true.

[bregma]

> my understanding is if you deduce something true from an assumption it means nothing.

Your understanding is not complete.

If you start from a set of assumptions and perform a series of logical deductions to reach a conclusion, you have proven that given the assumptions are true, the conclusion is true. You have a proof of correctness under the assumptions.

If you can go on to demonstrate your conclusion is false (say, with a single counterexample) then it will prove that at least one of your original assumptions is false. You now have some provably reliable knowledge .

[thaumasiotes]

>> my understanding is if you deduce something true from an assumption it means nothing.

> Your understanding is not complete.

> If you start from a set of assumptions and perform a series of logical deductions to reach a conclusion, you have proven that given the assumptions are true, the conclusion is true. You have a proof of correctness under the assumptions.

04091948 is completely correct here.

If you assume P and prove Q, then you've proven that P implies Q.

If you assume P and prove True, then you've proven that P implies True. This is the same thing as proving nothing, since everything implies True.

[QuesnayJr]

It's the article that has it backwards. You can deduce true from any premise. In terms of the Curry-Howard isomorphism, I can write a program from any input to the one-element type by throwing away the input and returning the one element.

I think the previous comment was alluding to "resolution", where you prove a statement true by assuming it is false, and then deriving a contradiction. That only works in classical logic, though.

[anandoza]

I think it's (very) poorly phrased, and what they meant by "logical deductions" was algebraic simplifications.

For example, if you already know x == 3 and your original "assumption" (not a great word choice here) is "x < 5 OR x > 20", you can simplify that to "3 < 5 OR 3 > 20" and then to "True OR False" and then the boolean literal "True", so you know the original expression "x < 5 OR x > 20" is True.

That's my best guess, at least.

[contravariant]

>my understanding is if you deduce something true from an assumption it means nothing.

That's not the case, even without axioms if you start at A and deduce B then this proves that "A => B". And usually you start with some axioms (i.e. statements that are true by definition; in the context of the article these are the types that have an implementation). Anything that follows from those is also true. At the end of the article the author stumbles upon the fact that you can add implementations / axioms for anything you want (however there's no guarantee that your theory will remain consistent).

>you need to deduce something false and thus the negation of your assumption is true.

Ironically it's precisely the reasoning "<contradiction> follows from B therefore not B" that's currently being questioned by mathematicians. Although in most context it is still a valid line of reasoning.

And what's entirely missing from the article is the distinction between true and provable. These aren't quite the same. Sure Goedel did prove that all statements that hold for every possible model (~implementation) of a theory are provable, but he also showed that no theory of arithmetic can have a unique model.

[thaumasiotes]

> That's not the case, even without axioms if you start at A and deduce B then this proves that "A => B".

As I already pointed out in this thread, you're not right here. It is true that if you start at A and deduce B you've proven A ⟹ B. But if you're deducing something true, it's not necessary to start with A. If B is true, then A ⟹ B for all A, so you've proven nothing you didn't already have. It is quite literally correct to say that "if you deduce something true from an assumption, it means nothing".

You can see a nice visual illustration of the meaninglessness of the premise by completing the proof of "A→B" from "B" at http://incredible.pm (session 2)

[thaumasiotes]

1. Assume (p ⋀ (q ⋁ ¬q))

2. Then (q ⋁ ¬q) [method of simplification]

3. Then True [(2) is a tautology]

4. Then (p ⋀ (q ⋁ ¬q)) is correct independent of assumption (1) [erroneous]

5. Then p [method of simplification]

[htns]

False of course implies true, but the deductions are supposed to be in reverse. So a chain of deductions could be P <= P' <= true where P is the original goal.

[thaumasiotes]

This interpretation is not compatible with the text of the article:

> If you need a quick refresher on logical True and False, here it is: The logical proposition True simply represents something that is true, like the statement 1 < 5. Any true statement like that by definition implies True. If we can start from an assumption and perform a series of logical deductions and reach True, then we know our original assumption is True, that it is provable. Conversely, any statement we know or can prove to be wrong (such as "bananas are a myth") implies False. If we can reach False at the end of a series of logical deductions from an assumption, our assumption is incorrect.

Showing that P implies False is a valid way to show that P is false itself. But showing that P implies True isn't a way to show that P is true. If you run things in the other direction, showing that P is implied by True really is a valid way to show that P is itself true, but showing that P is implied by False is not a way to show that P is false -- everything is implied by False.

[auggierose]

Yeah, that's what you get when you let computer scientists do math :-D

I hope it's just a typo, otherwise you should throw the article straight into the garbage.