Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What is logic?

aeon.co

Post reply on HN
Print view View original

51–60 of 67 posts

Re: What is logic?

#51

Post by danharaj »

mafribe wrote: post #30
tikhonj wrote: post #16

Earlier quoted context omitted.

On a slightly orthogonal note, I think that not only can you think of programming languages this way, but that you should —programming languages and formal logics are ultimately instances of the same general idea. I've found this to be a consistent and powerful view for reasoning about programs, programming languages, proofs and logics in a uniform sort of way. The Curry-Howard correspondence is an important idea tha…

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either. It seems to me that constructive proofs are a special class of programs, and fall under t…

> The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc.

No it doesn't. Each of those features leads to a different logic. You can even reason about the composition of logics via category theory to see how various features interact with each other.

> Classical logic doesn't really have wholly convincing CH-correspondences either.

Sure it does, first class continuations: http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf

I suppose you have the right to remain unconvinced.

Re: What is logic?

#52

Post by cscurmudgeon »

spacehacker wrote: post #42

I've been surprised to not find anything for ctrl-F "Bayes". It turns out that traditional deductive logic is simply a special case of applying Bayes rule in order to find out the state of some binary variables given the other variables in which the probabilities are only 0 or 1. See for example these examples from Barber's "Bayesian Reasoning and Machine Learning" (p. 39): https://i.imgur.com/W1b0Wem.png https://i.i…

Deductive logic is sort of like the machine code for reasoning. It encompasses everything, but it is hard to see in daily usage, just like machine code. Bayes Rule is just one part of it.

If you look at the Mizar mathematical library you will find a formalization of Bayes Rule using plain FOL.

In fact, one of my Logic II (an intermediate logic class) exercises was formalizing a version of Bayes' rule in classic first-order logic.

Re: What is logic?

#53

Post by cscurmudgeon »

pitaj wrote: post #3

From what I know, pure logic or even math are useless without assumptions. This is what reason and science give us: a standard set of axioms from which logic and math can lead us to useful conclusions.

You can't do science without logic. They are all highly intertwined.

Re: What is logic?

#55

Post by cousin_it »

westoncb wrote: post #20
cousin_it wrote: post #19

Gödel's arithmetization of logic is one hell of a beautiful mathematical idea, up there with linear algebra or probability theory. One of its big selling points for me was how easily it solves the unexpected hanging paradox. (The simplest arithmetization of the judge's self-referential statement is a statement about numbers that can be shown to be self-contradictory.) It's also cool how it turns Russell's paradox int…

Do you have a recommendation for a book that covers these topics that's technical but not necessarily a text book?

I really like Peter Smith's "Gödel Without Tears" lecture notes: http://www.logicmatters.net/resources/pdfs/gwt/GWT2f.pdf

Re: What is logic?

#56

Post by lngnmn »

metaphorm wrote: post #33
lngnmn wrote: post #4

A set of general rules for not losing a connection to reality. Could be used in reasoning or computer programming.

this is amusingly missing the point. logic is, by its nature, an abstraction away from reality. it's a set of specific (not general) rules for evaluating statements of language (whether that language is natural, mathematical, or artificial/computer) such that meaning can be disambiguated. "reality", whatever it is, has no such requirement that it can be expressed in unambiguous statements.

Syllogism is not general?

WTF am I reading?

Re: What is logic?

#57

Post by mafribe »

mkehrt wrote: post #48
mafribe wrote: post #30

Earlier quoted context omitted.

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either. It seems to me that constructive proofs are a special class of programs, and fall under t…

Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A. There's some connection between classical logics and concurrency, though it's hard to get at. You can use callcc to implement threads, and Getzen's classical sequent calculus has multiple conclusions. Here is a PHD thesis that uses modal logic to model distributed code in a CH fashion: http://www.cs.cmu.edu/~t…

   Non termination is modeled as false:
That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) about non-terminating computation.

The T. Murphy PhD doesn't deal with distribution because it lacks the key feature of distribution which is partial failure.

As far as I'm aware the work on modelling double negation by call/cc doesn't actually provide a 1-to-1 correspondence between programs and proofs. I've forgotten the details but I think only some programs come out being proofs.

Re: What is logic?

#58

Post by mafribe »

tikhonj wrote: post #36
mafribe wrote: post #30

Earlier quoted context omitted.

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either. It seems to me that constructive proofs are a special class of programs, and fall under t…

The point is that they're both formal systems of reasoning, not that they have exactly the same properties. The techniques and abstractions from both PL and formal logic often generalize well to both.

Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.

Re: What is logic?

#59

Post by mafribe »

danharaj wrote: post #51
mafribe wrote: post #30

Earlier quoted context omitted.

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either. It seems to me that constructive proofs are a special class of programs, and fall under t…

> The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. No it doesn't. Each of those features leads to a different logic. You can even reason about the composition of logics via category theory to see how various features interact with each other. > Classical logic doesn't really have wholly convincing CH-correspondences either. Sure it does…

   can even reason about the composition of logics
I'm not aware of a fully fledged approach to logical composition that tells me an interesting story about the combination of logics that arise in computation, I know that people work on this, but as far as I can see, this work is far from finished. Please point to papers if you know more than that.

    first class continuations
As far as I'm aware, Griffin's work, which was a stroke of genius, does not provide a 1-to-1 correspondence between classical proofs and programs. That's why even today, 1/4 of a century later, people work on CH for classical logic.

Re: What is logic?

#60

Post by empath75 »

fenomas wrote: post #50
alasdair_ wrote: post #29

Earlier quoted context omitted.

GEB is well worth a second attempt. It's one of the very few books that completely changed my worldview.

I read GEB a few years ago, and it struck me as a book full of ideas that would have transformed me had I been encountering them for the first time. I think the book may have been so influential that its big ideas had largely filtered out into places where I'd encountered them. If I'd read it at 19, say, I think it would have rocked my world. Note that I'm mostly talking about the book's first half (about incompleten…

I did read it at 19 and it did rock my world.
Post reply on HN