id: 1b114b2fc7b54ebe936649ac03fb7811
parent_id: 149b04507bbb41a2b53284beb2c3fe27
item_type: 1
item_id: fc9e4d47857b4515a6b6531b36cf3691
item_updated_time: 1683566782834
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"ies \"],[1,\"`\"],[0,\"M |= phi\"],[-1,\"\\\n\"],[1,\"`\\\nCompleteness: `\"],[0,\"M |= phi\"],[1,\"`\"],[0,\" imp\"]],\"start1\":3601,\"start2\":3601,\"length1\":25,\"length2\":43},{\"diffs\":[[0,\"implies \"],[1,\"`\"],[0,\"M |- phi\"],[1,\"`\\\n\\\nColloquially: if a proof system is sound, it is impossible to prove something that is not true. If it is complete, it is possible to prove all true things.\\\n\\\nMeng and Paulson talk, in their discussion of HOL translations, about the soundness of proofs. They say \\\"omitting types yields a compact result, but the resulting proofs can be _unsound_: that is, meaningless in higher-order logic.\\\" For instance, take the context and conjecture:\\\n\\\ndatatype two = a | b\\\nh : forall(x: two, x = a \\\\/ x = b)\\\n|- forall(x: nat, x = a \\\\/ x = b)\\\n\\\nThis is obviously false (in fact, not even well-typed). However, if we erase types:\\\n\\\nh : forall(x, x = a \\\\/ x = b)\\\n|- forall(x, x = a \\\\/ x = b)\\\n\\\nNow, our hypothesis is equal to our goal, and our proof is trivial. This proof is, however, \\\"unsound\\\", in the sense that it is a proof of something that is not true in the original logic.\\\n\\\nThe authors also discuss the soundness of translations. For instance, they call the fully-typed translation \\\"sound\\\", meaning that it does not produce problems that admit unsound proofs.\\\n\\\nNow, in the Encoding Monomorphic and Polymorphic Types paper, we get the following definitions of \\\"sound\\\" and \\\"complete\\\" translations:\\\n\\\n\\tA translation that translates problems Phi over signature Sigma to Phi' over Sigma' is _sound_ if the satisfiability of Phi implies the satisfiability of Phi'.\\\n\\t\\\nNow, this seems to me the exact opposite. This precludes our translation from making problems unsatisfiable, but that is not of primary importance to us. What we care about is that, once we have a proof in our target logic, that tells us something about the existence of a proof in our source logic. That is, if Phi' is satisfiable, so is Phi. This property they call \\\"completeness\\\", but MePo call such a proof \\\"sound\\\".\\\n\\\nFun, right?\"]],\"start1\":3641,\"start2\":3641,\"length1\":16,\"length2\":1801}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-05-08T17:27:38.270Z
created_time: 2023-05-08T17:27:38.270Z
type_: 13