re: G proof

If you interpret r, s, t, u as sets (might as well), then ⊳ is some sort of pointwise order (every element of r is greater than every element of s), and ⊏ (not <, oops) is the subset relation

Axiom 4 says that if r is pointwise greater than s and u is a subset of s, then r is pointwise greater than u, which makes sense

Axiom 5 says that there is a set r s.t. if there is a set pointwise smaller than z, then z is a subset of r

Personally I think ax5 isn't independent of ax1 and ax4

I bet Axiom 5 could be proven from the other axioms

I bet I can find a shorter proof

G proof

Looks like there's two relations, _ ⊳ _ and _ < _

The first is meant to be some sort of order and the second one is some sort of subtyping relation

Definitions:

- S r ≡ r ⊳ r
- C r ≡ ∃s. r ⊳ s
- O r ≡ ∀s. r ⊳ s

Axioms:

- ax1: ∀r. ∃v. v ⊳ r
- ax2: ∀r. ∀s. ∀t. (r ⊳ s) → (s ⊳ t) → (r ⊳ t)
- ax3: ∀r. ∀s. (r ⊳ s) → (s ⊳ r) → r = s
- ax4: ∀r. ∀s. (r ⊳ s) → (u < s) → r ⊳ u
- ax5: ∃r. ∀z. C z → z < r, i.e. ∃r. ∀z. ∃s. z ⊳ s → z < r

Let's see... ax1 says that there always exists a greater element, ax2 is transitivity, ax3 is antisymmetry, and ax4 and ax5... well I can't tell what < is meant to be

In any case the G theorem just says that there's a unique maximal element that's reflexive under ⊳

Anyway, and is and, or is or, nor is nor, so is implication, for is inverse implication, and yet is like the inverse of but

They're all coordinating conjunctions but it doesn't seem like for or so could be used to coordinate anything but independent clauses, i.e. not noun phrases

Might unironically listen to an 80s playlist https://www.youtube.com/playlist?list=PLahKLy8pQdCM0SiXNn3EfGIXX19QGzUG3

genitals, Coq

Okay people like this

But maybe you should ask yourself why you see what-you-don't-want-to-see in something that has never been related to what-you-don't-want-to-see...

(If the shape of the Coq logo makes you think to what-you-don't-want-to-see, maybe it's time to go to the doctor...?)

People like this annoy me so much

- pronouns
- he/him

- public acc
- @ionathanch

- website
- https://ionathan.ch

- birdsite
- https://twitter.com/ionathanch

Admin

Jon(athan)? | ionchy [jɑːnt͡ʃi] 🏳️🌈

MSc student in CS doing PL things 🇨🇦

@ionathanch on most places 🐦

PoGo: 8336 6654 0984

#WaterDrinker 💧

emoji boy of types.pl

I have been blessed with admin powers on this instance and I will do my best not to muck things up

pfp: https://picrew.me/share?cd=6rKy0AQ4I3

header: https://doi.org/10.1145/2578855.2537850

Joined Oct 2020