]>
Lambda the Ultimate - Comments
http://lambda-the-ultimate.org
CommentsenClassical logic appropriate only for a small number of axioms
http://lambda-the-ultimate.org/node/5164#comment-85984
Classical logic is appropriate only for a simple theory having a small number of axioms with strong evidence of consistency.
Practical Inconsistency Robust Direct Logic has only recently been invented for which inference engines are being developed. There is some work on previous less practical paraconsistent logics that are no fully inconsistency robust.Wed, 27 May 2015 23:45:08 +0000HewittMore information about AlbatrossClassical logic inappropriate?
http://lambda-the-ultimate.org/node/5164#comment-85983
You did not answer my question. I have chosen classical logic as the reasoning base for the proof engine in Albatross. Is this choice wrong for this purpose and why?
I don't know what "Inconsistent Robust Logic" is and I have never heard of it. Most theorem provers / proof assistants use either constructive logic or classical logic. To the best of my knowledge none has chosen the logic you propose. Why?Wed, 27 May 2015 19:26:23 +0000hbrandlMore information about AlbatrossSee book "Inconsistency Robustness" for published versions
http://lambda-the-ultimate.org/node/5136#comment-85982
See book "Inconsistency Robustness" for published versions of articles.
Also, there are numerous online videos that have been published that cover the material in the book.
PS. I am sorry that you have had a difficult time reading my articles. I would be happy to answer any specific questions that you might have.
PPS. Academic politics in this area of research can be very complicated as explained in one of the articles in the book.Wed, 27 May 2015 18:40:01 +0000HewittTypes are fundamental to both logic and computationClassical logic makes errors reasoning about inconsistent info
http://lambda-the-ultimate.org/node/5164#comment-85981
Classical logic makes errors reasoning about inconsistent information.
See <a href="https://hal.archives-ouvertes.fr/hal-01148501"> Invalid classical proofs using inconsistent information</a>Wed, 27 May 2015 18:30:42 +0000HewittMore information about AlbatrossProof by contradiction is fundamental to mathematics/reasoning
http://lambda-the-ultimate.org/node/5136#comment-85980
Proof by contradiction is fundamental to mathematics and reasoning in general.
For example, proof by contradiction is used in intuitionistic logic with he following rule:
<pre>
(Φ⊢Ψ,¬Ψ)⊢¬Φ
</pre>
In intuitionistic logic, ¬¬¬Φ is equivalent to ¬Φ. However, intuitionistic logic is not very useful in computer science because ¬¬Φ is not equivalent to Φ :-(
PS. Thanks for your interest in Inconsistency Robust Direct Logic :-)Wed, 27 May 2015 18:27:06 +0000HewittTypes are fundamental to both logic and computationI have just said that it is
http://lambda-the-ultimate.org/node/5164#comment-85979
I have just said that it is easy to verify that the logic used in Albatross is equivalent to classical predicate logic (by reviewing the documentation).
This does not mean that the correctness of the implementation of the Albatross compiler is easy to verify. But this applies to all proof assistants/theorem provers. E.g. the implementation of the Coq compiler is not verified either.
There is one technique which mitigates the situation: It is much easier to verify the correctness of a proof than to generate it. The Albatross compiler satisfies the "de Bruijn" condition because it generates for each proof a so called proof term and the verification that the proof term actually proofs the theorem is easy and contained in a very small fraction of the code. The Albatross compiler internally verifies the correctness of all proof terms before it enters the corresponding theorem into the database.
In principle the Albatross compiler could write the proof terms to file and an independent programm could verify that the generated proofs are correct.Wed, 27 May 2015 14:43:00 +0000hbrandlMore information about AlbatrossThanks for the counterpoint
http://lambda-the-ultimate.org/node/5167#comment-85978
Thanks for the counterpointWed, 27 May 2015 14:36:15 +0000BlaisorbladeComposite Replicated Data Types: eventually consistent libraries as non-leaky abstractions
It'd be nice to be able to
http://lambda-the-ultimate.org/node/5167#comment-85977
<blockquote>
It'd be nice to be able to tag/hide a subthread or move it into a new post when this happens.
</blockquote>
The Discourse forum platform offers a feature exactly for that, since it's been designed to foster good discussion practices (at least they say). I haven't enough insight to evaluate the Discourse claims critically, or to know how else it could help here.
Is there enough interest to open a discussion on the platform? Right now, I don't even see people complaining that LtU still requires HTML input rather than Markdown, which is the first source of technological friction with LtU for me.Wed, 27 May 2015 14:35:08 +0000BlaisorbladeComposite Replicated Data Types: eventually consistent libraries as non-leaky abstractionsFor instance, substitution
http://lambda-the-ultimate.org/node/5164#comment-85976
It is well known that substitution is a pain to get right, and a bigger pain to formally prove right. If you're writing a theorem prover, you know that, so I'll omit references. I also expect you to know that such bugs often go undetected for years.
However, you claim that verifying correctness of Albatross is "easy" without qualifying the statement the way I'd expect. How come?Wed, 27 May 2015 14:17:27 +0000BlaisorbladeMore information about AlbatrossAcademia
http://lambda-the-ultimate.org/node/5136#comment-85975
Prof. Hewitt, for all I know you might well be a genius. But I don't think that excludes you from the academic process, and I can't presume you don't know it since you provided a formalization of it.
So, if you want to challenge standard point of views, you write a paper (which you did) and submit it to peer review like everybody else. And if reviewers reject it, you take the extra effort to make your argument clearer, until you get it published by making it convincing enough. Not sure that's modeled in your formalization, but that's a standard part of the practice of science.
I say this because I've spent lots of time reading several of your papers, and I've never found the clarity which I've come to expect from good papers. I don't seem to be alone there.
For instance, why's the self-consistency proof of mathematics not published in a peer-reviewed venue? Why doesn't your paper cite a peer-reviewed and published formalization of direct logic when it first mentions it? If there is no such thing, why aren't you writing it?Wed, 27 May 2015 14:09:55 +0000BlaisorbladeTypes are fundamental to both logic and computationI have not the slightest
http://lambda-the-ultimate.org/node/5164#comment-85974
I have not the slightest idea what you are talking about.
Are you saying that classical logic is not adequate? But why?Wed, 27 May 2015 13:55:48 +0000hbrandlMore information about Albatrosssolves a real problem such as Facebook might have
http://lambda-the-ultimate.org/node/5167#comment-85973
Ironically, the second author was a <a href="http://link.springer.com/chapter/10.1007%2F3-540-45931-6_28">primary contributor to separation logic</a>, the secret sauce to the spin-out company <a href="http://www.eecs.qmul.ac.uk/research/impact/monoidics">Monoidics</a>, which was of sufficient interest to Facebook that <a href="http://www.theguardian.com/technology/2013/jul/18/facebook-buys-monoidics">they bought the company</a>.Wed, 27 May 2015 10:33:10 +0000jeremygibbonsComposite Replicated Data Types: eventually consistent libraries as non-leaky abstractionsInconsistency Robust Logic
http://lambda-the-ultimate.org/node/5136#comment-85972
I find proof by contradiction to be problematic, to me its not really a proof, but one of four states (proved, not proved, incomplete and inconsistent). Rather than adopt a four valued logic, I would rather keep the proof of negated statements separate, so they only get evaluated if needed, so you can prove "a" separately from "not a".
So I am starting to find inconsistency robust logic interesting (exclusion of proof by contradiction). However I am also interested in intuitionistic logic (exclusion of excluded-middle and double-negation).
I have a couple of questions:
What do you think about the intuitionistic fragment of inconsistency robust logic, has any work been done on this?
The proof methods (proof by contradiction, etc) are not part of the logic itself, but are metalogic? Is there a simple rule-based treatment of metalogic, or a classification of metalogic systems? Is inconsistency robust logic really a metalogic for classical-logic?Wed, 27 May 2015 09:11:31 +0000Keean SchupkeTypes are fundamental to both logic and computationClassical versus Inconsistency Robust Logic
http://lambda-the-ultimate.org/node/5164#comment-85971
The general form of the chaining rule is:
<pre>
(Φ∧(Φ⊢Ѱ))⊢Ѱ
</pre>
The following rule is valid <i>only</i> in classical logic:
<pre>
(Φ⊢Ѱ)⊢(Φ⇒Ѱ)
</pre>
because implication(i.e. ⇒) in Inconsistency Robust logic is much stronger than inference (i.e. ⊢) and in fact:
<pre>
(Φ⇒Ѱ)⊢(Φ⊢Ѱ)
</pre>
See <a href="https://hal.archives-ouvertes.fr/hal-01148501"> Inconsistency Robust Logic</a>Wed, 27 May 2015 00:17:06 +0000HewittMore information about AlbatrossI agree that the names pre-
http://lambda-the-ultimate.org/node/5164#comment-85970
I agree that the names pre- and postcondition give the impression of a time order. But note that the keywords are "require" and "ensure" and these don't impose a time order. The require clause gives a list of conditions under which the expressions in the ensure clause are valid.
In my opinion this reads well for proofs.
The term pre- and postconditions should be used only for procedures.Tue, 26 May 2015 21:29:36 +0000hbrandlMore information about Albatross