Re:There's a mathematician in your compiler
by thaumasiotes on Tuesday March 31, 2020 @09:43AM
(#22737437)
>> 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.
> 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.