4 ms·

Are You Using the Right Axiomatic System?

42 points by p4bl0 16y ago

erehweb 16y ago
The password security checker at http://estatis.coders.fm/password-security-checker/ http://estatis.coders.fm/password-security-checker/ is also good - check the Terms and Conditions
rheide 16y ago
It's funny because it's true (in the Falso axiomatic system). It's sad because I get it.
archgoon 16y ago
I'm working on a proof certified operating system. The original plan was to use Coq to verify the code, but Falso looks like an excellent, not to mention faster, alternative. It's already verified the correctness of my code, which is a vast improvement over the string of errors I got when running it through Coq and Isabelle. ---- This post has been verified by Falso for correctness.
gosub 16y ago
There is a comparison table on the page, it says that in ZFC less than 50% of the statements are true. A quick google search gave me nothing, does anybody know where I can learn more about this statement? Or is it a meta-joke?
- omaranto 16y ago
  It's a joke, but a slightly wrong one, I think: they should say "provable" instead of "true". For every true statement it's negation is false and viceversa, so exactly half of all possible statements are true. In a system like ZFC not all of the true statements are provable, so less than 50% are provable. (Also, less than 50% are refutable --this means provably false--, and the non-provable, non-refutable statements are called undecidable.)
  - a3_nm 16y ago
    I don't understand your reasoning to justify that "half of all possible statements are true". It seems to me that of the undecidable statements, some (such as those of Gödel's construction) are true or false, but that some simply have no truth value. Did I get something wrong? [Indeed, this is all assuming that ZFC is consistent. Thanks mjw.]
    - p4bl0 16y ago
      That's also how I understand it. Anyway, you people should upvote a3_nm, he is the one who did the job (for Falso and the Security Password Checker), I only encourage him and host the pages :-).
    - omaranto 15y ago
      I wouldn't say undecidable statements have no truth value. In any given model of set theory each statement is either true or false. If something is provable it is true in every model, and if something is refutable it is false in every model. Undecidable statements can't be proved to be either true or false within a given proof system, but (1) in any given model are either true or false, as I said, and (2) can sometimes be shown to be true (or false) by arguments outside of the proof system considered.
  - mjw 16y ago
    Assuming it's consistent, that is! Perhaps they shouldn't be so ready to belittle their competitors -- you never know, ZFC might yet turn out to share all the advantages of Falso :)
  - chalst 16y ago
    It's not mathematically correct: both all statements of ZFC and the provable have the same cardinality: there's no sense to "half of statements" in ZFC.
    - omaranto 15y ago
      Again it's a joke, so let's not take it too seriously but I think the sense in which it is half is not cardinality (that would be silly, as you point out), but density. Look at the probability that a random statement of length at most n is true. Since for every statement it's negation has practically the same length and the opposite truth value, the probability should tend to 1/2 as n goes to infinity.
- p4bl0 16y ago
  Omaranto already answered, so I'll just add to links: https://secure.wikimedia.org/wikipedia/en/wiki/G%C3%B6del%27s_incompleteness_theorem https://secure.wikimedia.org/wikipedia/en/wiki/G%C3%B6del%27... https://secure.wikimedia.org/wikipedia/en/wiki/List_of_statements_undecidable_in_ZFC https://secure.wikimedia.org/wikipedia/en/wiki/List_of_state...
erehweb 16y ago
The comparison chart is incorrect, though. ZFC can prove its own consistency... according to Falso, at least.
anonymoushn 16y ago
Rafee Kamouna already proved that ZFC is the same as Falso: http://kamouna.wordpress.com/ http://kamouna.wordpress.com/
Natsu 16y ago
I suggest avoiding zebra crossings if you use this on any theorems involving the colors black and white.
cafard 16y ago
Reminds me rather of an old essay called something like "The Runabout Inference System, Or Notes on 'Tonk'.

42 points by p4bl0 16y ago

The password security checker at http://estatis.coders.fm/password-security-checker/ http://estatis.coders.fm/password-security-checker/ is also good - check the Terms and Conditions

rheide 16y ago

It's funny because it's true (in the Falso axiomatic system). It's sad because I get it.

archgoon 16y ago

I'm working on a proof certified operating system. The original plan was to use Coq to verify the code, but Falso looks like an excellent, not to mention faster, alternative. It's already verified the correctness of my code, which is a vast improvement over the string of errors I got when running it through Coq and Isabelle. ---- This post has been verified by Falso for correctness.

gosub 16y ago

There is a comparison table on the page, it says that in ZFC less than 50% of the statements are true. A quick google search gave me nothing, does anybody know where I can learn more about this statement? Or is it a meta-joke?

omaranto 16y ago
It's a joke, but a slightly wrong one, I think: they should say "provable" instead of "true". For every true statement it's negation is false and viceversa, so exactly half of all possible statements are true. In a system like ZFC not all of the true statements are provable, so less than 50% are provable. (Also, less than 50% are refutable --this means provably false--, and the non-provable, non-refutable statements are called undecidable.)
- a3_nm 16y ago
  I don't understand your reasoning to justify that "half of all possible statements are true". It seems to me that of the undecidable statements, some (such as those of Gödel's construction) are true or false, but that some simply have no truth value. Did I get something wrong? [Indeed, this is all assuming that ZFC is consistent. Thanks mjw.]
  - p4bl0 16y ago
    That's also how I understand it. Anyway, you people should upvote a3_nm, he is the one who did the job (for Falso and the Security Password Checker), I only encourage him and host the pages :-).
  - omaranto 15y ago
    I wouldn't say undecidable statements have no truth value. In any given model of set theory each statement is either true or false. If something is provable it is true in every model, and if something is refutable it is false in every model. Undecidable statements can't be proved to be either true or false within a given proof system, but (1) in any given model are either true or false, as I said, and (2) can sometimes be shown to be true (or false) by arguments outside of the proof system considered.
- mjw 16y ago
  Assuming it's consistent, that is! Perhaps they shouldn't be so ready to belittle their competitors -- you never know, ZFC might yet turn out to share all the advantages of Falso :)
- chalst 16y ago
  It's not mathematically correct: both all statements of ZFC and the provable have the same cardinality: there's no sense to "half of statements" in ZFC.
  - omaranto 15y ago
    Again it's a joke, so let's not take it too seriously but I think the sense in which it is half is not cardinality (that would be silly, as you point out), but density. Look at the probability that a random statement of length at most n is true. Since for every statement it's negation has practically the same length and the opposite truth value, the probability should tend to 1/2 as n goes to infinity.
p4bl0 16y ago
Omaranto already answered, so I'll just add to links: https://secure.wikimedia.org/wikipedia/en/wiki/G%C3%B6del%27s_incompleteness_theorem https://secure.wikimedia.org/wikipedia/en/wiki/G%C3%B6del%27... https://secure.wikimedia.org/wikipedia/en/wiki/List_of_statements_undecidable_in_ZFC https://secure.wikimedia.org/wikipedia/en/wiki/List_of_state...

erehweb 16y ago

The comparison chart is incorrect, though. ZFC can prove its own consistency... according to Falso, at least.

anonymoushn 16y ago

Rafee Kamouna already proved that ZFC is the same as Falso: http://kamouna.wordpress.com/ http://kamouna.wordpress.com/

Natsu 16y ago

I suggest avoiding zebra crossings if you use this on any theorems involving the colors black and white.

cafard 16y ago

Reminds me rather of an old essay called something like "The Runabout Inference System, Or Notes on 'Tonk'.