Comment by pcfwik

Open in a window
Comment

Comment by pcfwik

I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing.

However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong:

> Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...]

You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.)

What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic.

Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.

Replies pcfwik · 18d
Open on HN
Loading the discussion…

Domain filters

Stories from these domains are hidden from every list. Subdomains match too: blocking substack.com also hides danluu.substack.com. The list is kept in this browser only.

Help

Keyboard

j / k
Move down and up the story list. The arrow keys scroll whatever has focus.
Enter
Open the marked story in a window.
]
Open the next story in the list in place of the one in front. Back returns to it.
p
Pin or unpin the marked story, which keeps it in Pinned.
n / N
Move to the next or previous top-level comment in the window in front.
c
Collapse or expand that comment.
f
Hide or show the story list.
Esc
Close a menu or this help.
Access key m
Go to the menu bar. Most browsers take it with Alt on Windows and Linux, and Safari with Control and Option.
?
Show this help.

Windows

Each story opens in a window holding its article above its discussion; drag the bar between them to share the room differently. A window can be moved by its title bar, resized from any edge, snapped to a half or a corner by dragging it there, maximised, or minimised to the bar at the foot of the page. Open several stories to compare them, and switch between them from that bar. A window's Next story link reads on down the list in the same window.

A link in a comment or an article to another Hacker News or Lobsters thread opens that thread in a window too. A link to a single HN comment opens the comment above its replies.

While a story's window is in front, the Story and Discussion menus in the menu bar hold its commands: pinning, Next story, sorting, collapsing every thread, jumping to the first new comment. Each window also remembers where you were in its article and discussion, so a reload, or Back to a story that Next took you past, finds your place again. Closing a window forgets it.

The whole arrangement lives in the address, so a bookmark or a shared link brings it back, and Back undoes the last change. Moving between Hacker News, Lobsters, their lists, Pinned and Find changes only the list, and leaves the windows open.

The list

The pin at the start of a row keeps the story in Pinned, and the cross at its end hides it. Pinned can be narrowed by words in the title, site or author, by source, and to the stories you haven't opened yet, and ordered by when you pinned them, by points or by comments; the filters are part of the address, so a filtered view can be bookmarked. Scroll past the end of the list to load more. Domain filters, in the View menu, hide every story from a site.

Applets

The Applets menu in the menu bar holds three tools, each a window of its own. Replies to me takes your Hacker News user name and lists the replies to your last thirty comments and stories, checking again every three minutes while it is open, and marking what is new since you last marked them read. Look up a user opens a profile on Hacker News or Lobsters, with their submissions and recent comments, as a commenter's name in any discussion does; the bar at the top of a profile looks up someone else in the same window, and Back returns to the one before. Who is hiring? filters the posts of HN's monthly hiring threads by the words you type.

They read only what the sites publish to everyone, so none of them asks for a login, and your user name stays in this browser.

Find

Find takes any link and lists every time it was submitted to Hacker News and Lobsters, so you can read each discussion of it.

About

YAVCHN never sees your Hacker News or Lobsters login. The discussion is fetched from each site's public API; to vote or reply, follow the link above the discussion, or the arrow beside a comment, to the source's own site. Pins, hidden stories, filters and layout are kept in this browser only.

Open source: github.com/paulmooreparks/yavchn. Built with PUDL.