4 ms·
Do they have a strong type system? Maybe I just haven't gotten to that. My issue is that, there doesn't seem to be any rules for "evaluating" a proof to see if
by quasarj 3y ago
Do they have a strong type system? Maybe I just haven't gotten to that. My issue is that, there doesn't seem to be any rules for "evaluating" a proof to see if it is valid. Everything seems subjective? Maybe I'm just missing something. But coming from programming, I'm obviously used to a situation where I can put my code through a mechanical evaluator which will tell me if it works. Or at least, will tell me if the syntax is right!
- lying4fun 3y agoWhen you proove something you are esentially prooving that a statement logically follows from some other statement(s) for which we know that are true You can evaluate the validity of a proof by checking the truthfulness of every statement which was used to argue that the proof holds Miniature example of a proof with relaxed rigor: Proove that 3+0=3 Proof: The above statement is a direct consequence of the additive identity axiom which states that x+0=x, if x is a real number. So the only thing we need to check is if 3 is a real number, and we know that it is. The statement holds, end of proof So to check the validity of this proof you could check if that axiom really exists and check if 3 is a real number, if some of those is false than the proof is invalid Edit: Or imagine that you have a DB full of axioms, theorems, prooven statements which you can use to proove a given statement. Then you could proove something by just referencing those. Eg. in the example above lets say that the neutral identity axiom has id 3, and the fact that 3 is a real number has an id 103. Then I could just say since 3 and 103 3+0=3