The Nineteenth Byte

Neil

12:06 AM

@ASCII-only How am I supposed to be evaluating π to 200 decimals? I thought perhaps Ｉ▷Pi⟦φ⟧ but that just crashes

Downsheep

12:35 AM

@Riker @ConorO'Brien TF2?

Destructible Lemon

1:23 AM

we say that a language is based on its implementation, but this implementation depends on it's implementor languages implementation

hm

what if you had a program file that is an interpreter, and given its own interpreter source, the language implements another language

hm. polyglot with language A and B. in A, it interprets B, in B, it interprets A

would be cool

@DJMcMayhem >:( why does the people's python have a hardcoded inverted dictionary instead of deriving it programmaticaly

Pavel

._. just tried to use xdotool on TIO

Not sure what I expected would happen

DJMcMayhem

1:42 AM

@DestructibleLemon I don't know, I didn't design it

Downsheep

@Poke Bill explicitly says "Cybersecurity active defense measures that are designed to prevent or detect unauthorized computer access" not sure what EFF is aying

quartata

@Downsheep That's what it currently reads

oh wait

Downsheep

it was last amended march 29

quartata

no sorry, misread it

Downsheep

before EFF article

quartata

1:52 AM

@Downsheep I meant that's what the section of the law read, but just noticed the underline so that's a new part

well I don't think "Cybersecurity active defense measures that are designed to prevent or detect unauthorized computer access; or" is referring to white hat

I think it's referring to anti-virus and automated things

hence active defense measures

Downsheep

@quartata It explicitly specifies "person" though

Also, I doubt a white hat hacker would be prosecuted for violating that section and I even more doubt that they wouldn't win that case

quartata

writing an anti-virus that violated it would still make you liable

hence the exemption

@Downsheep hell yeah they'd try to prosecute someone for it

winning is a different story

Pavel

Does anyone know how to send a mouse scroll event with xdotool? I can find how to do clicks and movement but not scroll.

Downsheep

@quartata how do you back up this claim

quartata

@Downsheep i guess you might not know about HB1630

Pavel

1:59 AM

Neither do I, please elaborate

quartata

basically made it illegal to use a "screen name" on the internet.

Downsheep

@quartata which state

quartata

georgia

Pavel

._.

quartata

georgia does not have a good track record on these things and frankly they'd probably prosecute just to piss off EFGA. they're not going to let people off the hook because of "good intents"

now I don't live there and this was a long time ago, I don't know

Downsheep

2:02 AM

@quartata that's a bit of a stretch

quartata

"if such data uses any individual name ... to falsely identify the person"

I know it's dense but it's there

Downsheep

it means you can't intentionally claim to be someone else to be able to use copyrighted/trademark info

@quartata please read the full sentence

quartata

the full sentence does not matter, it's commas. it's an OR

Downsheep

> individual name, trade name, registered trademark, logo, legal or official seal, or copyrighted symbol

which one of these is screen name

quartata

"individual name"

Downsheep

2:04 AM

that means someone else's actual name

it you must knowingly and intentionally do it

quartata

it does not specify legal name

and "intent" doesn't work that way

Downsheep

no but good luck to the prosecutor who is able to say xXGoatsRockXx is someone's real name

@quartata point is people distort reality and give shocking claims while quietly tucking away the important parts

quartata

well it was ruled unconstitutional in 1997 so maybe you should take it up with a federal court

original complaint: old.ef-georgia.org/hb1630/complt01.html

Downsheep

@quartata wow

quartata

yeah sorry it's long

but there's some better analysis than I can provide

ngn

2:10 AM

@Pavel xdotool click 4 # 4 for scroll up and 5 for scroll down

Pavel

@ngn Thanks

quartata

@Downsheep the crux of the second half of the complaint: if you post a link to, say, google.com, that counts as using their trademark under the act

since it's there textually in the URL

and the bill doesn't give a fuck about fair use judging by the phrasing

> All laws and parts of laws in conflict with this Act are repealed.

god card

Destructible Lemon

law makers kinda suck

quartata

that's why we have the judicial system

it does serious work

good stuff

Downsheep

^^^^ this is why spreading misleading information is bad

quartata

2:14 AM

hm?

Destructible Lemon

oh that reminds me... the cheese and stuff being illegal in florida technically

i think i said it earlier in chat

Downsheep

@DestructibleLemon .___. link?

Pavel

So I made a keybind with xbindkeys -f <customkeybindfile> , how do I then unbind these keys?

Destructible Lemon

Tyramine

Tyramine ( TY-rə-meen) (also spelled tyramin), also known by several other names, is a naturally occurring trace amine derived from the amino acid tyrosine. Tyramine acts as a catecholamine releasing agent. Notably, it is unable to cross the blood-brain barrier, resulting in only non-psychoactive peripheral sympathomimetic effects following ingestion. A hypertensive crisis can result, however, from ingestion of tyramine-rich foods in conjunction with monoamine oxidase inhibitors (MAOIs). == Occurrence == Tyramine occurs widely in plants and animals, and is metabolized by various enzymes, including...

it's not enforced though

it's banned along with many of its derivatives, for being a hallucinogen (it's not), and it is present in very very many foods and stuff, so they technically are illegal

Downsheep

i hope we can all agree that drug laws are stupid as-is

Destructible Lemon

2:18 AM

yes

Dennis

@Pavel Kill xbindkeys.

user202729

@DJMcMayhem for replacing the main and meta. Chat is not really a part of SE. (or at least I think so)

Pavel

@Dennis Thanks, you're a godsend

user202729

(BTW meta.stackexchange.com/questions/60588/chat-requirements is there any site with <20 rep requirement to chat?)

Pavel

The Stellaris creators didn't seem to take into account that not everyone has a proper mouse so you can't really play without a scroll wheel.

user202729

2:30 AM

@Pavel You can emulate the mouse and then slow down the game by 10x, but then it's boring...

Apparently I have not read the sandbox FAQ...

Pavel

@user202729 Well that's kinda what I just did. I bound page up/down to send mouse scroll commands

user202729

> It is ok if your question is still incomplete. --- Sandbox FAQ

Anonymous

2:58 AM

@user202729 Incomplete as in "I haven't hashed out all of the details yet", not "I put literally 0 effort into this"

user202729

I won't argue about that anymore. Just a suggestion, make it more explicit.

Anonymous

Most things on meta could be improved by making them more explicit

user202729

Numbers with the property you mention are known as normal numbers. An infinite decimal expansion, even if non-periodic, doesn't imply normality. 0.101001000100001... is a counterexample. — Dennis ♦ 13 hours ago

Why +14 :/

Dennis

Because as wrong as my comment is, the challenge is still wronger.

DJMcMayhem

Wait, what's wrong about your comment?

It seems right to me

Dennis

3:05 AM

@Dennis Normal is a much stronger condition (all-uniform vs all-exist) — user202729 13 hours ago

Appears to be a common mistake.

I was about to incorrectly type the same (numbers like that being normal) :-D — Luis Mendo 13 hours ago

user202729

DJ also upvoted that (I guess?)

Downsheep

3:29 AM

Oh god. All fortune 500 companies use npm

Destructible Lemon

4:04 AM

how do you prove a number is normal or uniform?

user202729

AFAIK pi has not been proven to be normal.

Anonymous

@DestructibleLemon It's very difficult to prove that a number is normal. Basically you have to connect the representations of the number in all bases b >= 2 to outputs of certain classes of FSMs.

Destructible Lemon

hm. how about containing all strings?

user202729

In which base?

Anonymous

@DestructibleLemon Similarly difficult.

Destructible Lemon

4:10 AM

hm. some are simple though i think

Anonymous

Some are simple because they're constructed to exemplify the property

Destructible Lemon

like if they have the property by definition

Anonymous

Like the Champernowne constant

Destructible Lemon

@Mego weren't constructed for ones starting with 0s

user202729

(that has only been proven to be normal in base 10 AFAIK)

Destructible Lemon

4:11 AM

but those are included as well

@user202729 not normal i'm pretty sure

1 hour ago, by Dennis

@Dennis Normal is a much stronger condition (all-uniform vs all-exist) — user202729 13 hours ago

Anonymous

@user202729 The Champernowne constant, written using base-b digits, is normal in base b

Destructible Lemon

hm

Anonymous

It's an open question whether or not C_b is normal in base k != b

Destructible Lemon

weird

i don't really understand what normal is then

or are people confused with all-uniform vs all-exist

what's the term for all-exist

user202729

I don't think there is a term for all-exist.

@DestructibleLemon Normal is (simply normal) in all bases >=2.

Anonymous

4:13 AM

Normal means that the digits follow a uniform distribution - all runs of digits of length [1, inf) are equally likely to exist as any other run of the same length

Anonymous

By definition, every normal number satisfies the all-substrings-exist property

user202729

In all bases.

Destructible Lemon

how is the champernowne constant normal then

user202729

(Why not?) (note that it's only normal in its base)

Destructible Lemon

because of like, not seeming like it would be very normal

very well distributed

Anonymous

4:17 AM

@DestructibleLemon In 0-9, each digit appears once. In 10-99, each digit appears 19 times. In 100-999, each digit appears 280 times. You can see the trend.

user202729

Both those versions can be considered "uniformly random" at each step, while they may produce different resulting distribution. Are they equivalent or which one do you want? — user202729 2 days ago

Destructible Lemon

what about strings starting with 0?

Anonymous

@user202729 The method of production for uniform sampling is irrelevant - all that matters is that every output has equal, finite, positive probability.

user202729

> This should uniformly random (i.e. a 50/50 chance of each direction), or as close to uniformly random as you can get on normal hardware.

Does the latter method satisfy that?

No, those 2 methods produce different distribution. (if I calculated correctly)

Destructible Lemon

strings starting with 0 only occur after specific numbers

user202729

4:22 AM

@user I think they are equivalent, I would accept any — nicael yesterday

Destructible Lemon

0000 must occur less than 1111 i think

user202729

But they are not. (...) what to do with the challenge now?

@DestructibleLemon Note that normal numbers only define the probability.

Destructible Lemon

yes but

probablity is less for 0000

Anonymous

@user202729 Generating a sequence of n bits by performing a Bernoulli trial for each bit is no different than generating a sequence of n bits by sampling a uniform distribution of n-bit sequences.

user202729

If they only differs by a constant or a sublinear factor it doesn't affect the probability.

@Mego (what are you replying to?)

Destructible Lemon

4:24 AM

does 0 not occur less than 1?

user202729

But that particular challenge requires the lines to be non-self-intersect.

@DestructibleLemon Sublinear factor.

(correct? Let me count it)

Destructible Lemon

i don't get it

Anonymous

@DestructibleLemon Any string of all zeroes occurs exactly 1 time less than any other string of the same length. Since we're dealing with an infinite number of strings, the limit is still the same.

Destructible Lemon

ok that makes sense i guess

Anonymous

@user202729 Sampling with rejection is also no different from sampling from a distribution containing only valid values

Destructible Lemon

4:27 AM

@Mego plus time

Anonymous

@DestructibleLemon Depends on how quickly the rejection can be done :P

user202729

I don't get your point.

For example, consider n=3.

A possible result can be >>>/vvv corresponds to

####
#
#
#

There are 4 valid answers matching the glob >>?/vv?, but only 3 valid answers matching >v?/vv?.

The first method makes the probability of getting a >>?/vv? 4/3 times larger than the >v?/vv? while the second method makes the probability equal.

So, they're different. (any flaw?)

Anonymous

Consider the following: Alice and Bob want to generate uniformly random sequences of 0s and 1s of length 8, where there are no consecutive 0s. Alice picks a uniform random bit to start. For each of the next bits, if the previous bit was a 1, she picks another uniform random bit. If the previous bit was a 0, she picks a 1. Bob picks a random number between 0 and 255 (inclusive), and rejects it if its binary representation contains consecutive 0s. Both are uniformly random and follow the rules.

Anonymous

I haven't read the challenge, so I don't know if there are other complications that would change the answer. However, based off of the general questions you've asked in here, both strategies should produce random sequences chosen uniformly.

user202729

wait a minute let me calculate the probabilities

First, the number of sequences with length (n) is Fib(n+1).

Anonymous

4:35 AM

Oh man I just realized that I was wrong about Alice's method

user202729

And there are Fib(n) sequences with length (n) starting with (1) and Fib(n-1) sequences with length (n) starting with (0).

Destructible Lemon

@user202729 oh it's like that stair thing isn't it

Anonymous

Consider 2-bit sequences. 01 has a 50% probability, while 10 and 11 have 25%.

Anonymous

Basically it's Monty Hall :P

Destructible Lemon

i was gonna say it seemed wrong

@Mego 2 bit sequences?

Anonymous

4:37 AM

Ok so the method I said for Alice is wrong, but I don't think that's the method that was being described anyway

Anonymous

@DestructibleLemon Yes, thanks, I'm tired

user202729

The linked challenge has a similar problem -- the 2 ways to interpret the challenge produces different distribution.

Destructible Lemon

speaking of Alice, have you ever played Alice chess?

user202729

No.

13

A: Standard Loopholes Pertaining to [underhanded]

Merge the answers and migrate them here ... or anywhere with the underhanded tag that can be found by people who are still interested in the early history of PPCG. I think these answers are of historical values and should be kept, just not in a way that interferes with the normal browsing of pa...

Anonymous

@quartata That left join is unnecessary - you're selecting from the many side of the many-to-one relationship, so an inner join will suffice

user202729

4:40 AM

It has 13 upvotes. Someone should do that?

Destructible Lemon

@user202729 it's nice. the original way to play requires two boards, but you can play it with coins under pieces on one board or something to show which board each piece is in, whether it has a coin or not

ASCII-only

4:59 AM

@Neil Try it online! (this is a number though so you'll have to cast it to use it as a string)

user202729

Everytime someone says "no built-in" I complains on the challenge. Everytime someone uses built-in I complains on the answer. >.<

I need a better solution.

ASCII-only

@user202729 ...

user202729

Or just hope that people will write nontrivial challenges.

user202729

6:13 AM

@cairdcoinheringaahing Hexagony, 7 bytes.

ASCII-only

6:25 AM

@Mego on the other hand there's me who's most likely doing unit tests completely wrong (i don't think 100 asserts in one method is a good thing lol)

user202729

100 asserts in one method is definitely a good thing.

ASCII-only

:|

Pavel

Unit tests are just collections of assertions. Having more generally means you've covered more cases.

ASCII-only

@Pavel not in my case lol

New Main Posts

7:07 AM

0

Q: Sum of five cubes

Given an integer, output five perfect cubes whose sum is that integer. Note that cubes can be positive, negative, or zero. For example, -10 == -27 + -27 + 125 + 0 + -81 so for input -10 you could output [-27, -27, 125, 0, -81], though other solutions are possible. Note that you should output t...

New Main Posts

8:37 AM

4

Q: Interval Notations

Challenge: Input: Two integer parameters a and b (where a<b) Output: Output or return this text, where a and b are filled in: (a,b) = ]a,b[ = {a<x<b} = {a<x&&x<b} = a+1..b-1 [a,b) = [a,b[ = {a<=x<b} = {a<=x&&x<b} = a..b-1 (a,b] = ]a,b] = {a<x<=b} = {a<x&&x<=b} = a+1..b [a,b] = [a,b] ...

code-golf string number integer

user202729

@MDXF This should be input && (mem %= input).

Also why do you set the code page but never use them...

ASCII-only

8:54 AM

@user202729 link pls

user202729

@ASCII-only github.com/aaronryank/Cubically/…

ASCII-only

@user202729 :||||

user202729

The official interpreter seemed to be lying about that it supports SBCS. shhhhh :P but congrats on winning the bounty! — MD XF Mar 20 at 3:21

(come on why does it only get 10 upvotes)

caird coinheringaahing

@user202729 Didn't you hear them, shhhh! :P

ಠ_ಠ It annoys me that there are currently 4 code-golf challenges with 99 votes, and I've upvoted all of them

user202729

downvote all of them (no I won't)

Improper quine?

0

A: Golf you a quine for great good!

J, 1 or 2 bytes 6 Will output 6, but it also adds a trailing newline, if the newline is counted then adding a newline to your own program makes them the same. algorithmshark kinda mentioned this in passing, but I wanted to draw more attention to this solution

New Sandboxed Posts

9:47 AM

0

A: Sandbox for Proposed Challenges

Polyglot Communication Write a polyglot that takes no input and runs in 2 different programming languages, that outputs the name of language B when run in language A and outputs the name of language A when run in language B. Example Program runs in the languages Python and C#. Outputs C# when...

caird coinheringaahing

in Jelly Hypertraining, 2 mins ago, by caird coinheringaahing

CMC: Given an integer n, return one distinct, consistent value if n is semiprime, and a different value if n is not semiprime. However, the Jelly ordinal of each character in your program must also be semiprime.

user202729

10:49 AM

Jelly, 23 bytes.

ATaco

o/

Leaky Nun

23 bytes to check semiprime :o

ATaco

@cairdcoinheringaahing RProgN 2, 2 bytes aL

ATaco

11:11 AM

You are correct.

But that was not the same CMC.

21 hours ago, by caird coinheringaahing

CMC: Output 26 without numbers in your source code

New Sandboxed Posts

0

A: Sandbox for Proposed Challenges

Make a Emergency Corridor codegolfacii-art In some nations there are recommendations or laws on how to form emergency corridors on streets that have multiple lanes per direction. (In the following we only consider the lanes going in the direction we are travelling.) These are the rules that hol...

H.PWiz

11:41 AM

@LeakyNun Can you give the solution to your last CMC please?

The one about functions, (nat -> bool) -> nat

New Sandboxed Posts

12:11 PM

0

A: Sandbox for Proposed Challenges

Rotate the character Find the most similar upside-down character of the input char. Here "similar" means, the amount of pixels where two image differ is lowest You can use default font, set font name or take font file as font input, but no directly input font object. [to-do: maybe rewrite] Sh...

Leaky Nun

@H.PWiz math.andrej.com/2007/09/28/…

4

I'm not sure I understand everything

but every computable function is continuous

here the nat -> bool type has the Cantor set topology

and nat has the discrete topology

so every function is locally constant

H.PWiz

I was hoping there would be some genius simple solution :(. Now I have to do some reading

Leaky Nun

and we search for counter-examples starting from the first digit

so given two functions f and g

we want to find a sequence of bool, called a_n, for which f(a_n) != g(a_n)

we start from the all-zero sequence

no we don't

the recursion algorithm is this:

for a predicate p, we want to find a sequence a_n for which p(a_n) is true

if there is some example starting with zero (recursion!), then set a_0 = 0

otherwise, set a_0 = 1

H.PWiz

1:37 PM

@LeakyNun I think I understand it, that is really cool stuff. The find_viii left in a comment is also awesome. I understand how all of it works and terminates, but I'm still surprised that it actually does...

Leaky Nun

@H.PWiz nice!... now you can explain it to me

H.PWiz

Maybe, any questions?

Leaky Nun

so how does the recursion work

and why does it terminate

H.PWiz

Perhaps it's worth working through a simple example, like equal (\a->23) (\a->if a(2)==Zero then 0 else 23)

Which boils down to computing forsome(\x -> ((\a->23)x) ≠ ((\a->if a(2)==Zero then 0 else 23)x))

Then we do find(\x -> ((\a->23)x) ≠ ((\a->if a(2)==Zero then 0 else 23)x))

(I'll be using find_i for this)

Leaky Nun

ok

H.PWiz

1:45 PM

Now forsome(\a -> p(Zero # a)), will jump back into find with the new predicate (\a -> p(Zero # a))

Which is equivalent to (\x -> ((\a->23)x) ≠ ((\a->if a(1)==Zero then 0 else 23)x))

Then, one more step goes to (\x -> ((\a->23)x) ≠ ((\a->if a(0)==Zero then 0 else 23)x))

If we chose to add another Zero at the start, they will not be equal so , if the above is p, forsome(\a -> p(Zero # a)) will return True and put us in the first branch.

I need to think for a bit...

The main part of the reason that this works is that find p will find a function that satisfies p (if one exists), but it does not need to full evaluate it

This is because p is guaranteed to only require a finite amount of information from the function

My example would perhaps be clearer if I chose a(2)==One, but the affect is the same:
whenever forsome first returns a bool, which it always has to (because p takes a finite amount of the function), we get the first part of the function. And then call find again to get the rest of the function

Leaky Nun

2:16 PM

nice

H.PWiz

A simplification of (\x -> ((\a->23)x) ≠ ((\a->if a(2)==Zero then 0 else 23)x)) to (\x -> 23 ≠ (if x(2) == Zero then 0 else 23) and then to (\x -> x(2)==Zero) also makes it easier

Leaky Nun

beta reduction

H.PWiz

I thought that was Eta reduction

Leaky Nun

eta is \a -> p a = p

H.PWiz

I was thinking of (\a->23)x --> 23 then

Leaky Nun

2:22 PM

that's beta reduction

H.PWiz

Uhh, you're right. They still look a bit the same to me :/

Leaky Nun

one involves the removal of a bracket

I mean, those reductions are too intuitive that they look the same

Poke

2:35 PM

what are some crazy reasons linkedhashmap.remove(validKey) might not modify a map in java

do i need to worry about local thread caching

caird coinheringaahing

@Poke The fact that it's Java?

H.PWiz

@LeakyNun the start of this talk explains it quite well. (maybe not) ... didn't actually listen to it

Leaky Nun

@H.PWiz cool, I'll watch it later

on the other hand, that blog page has some dank posts

H.PWiz

on the other hand?

Leaky Nun

eh

I mean

in other news

me englis no gud

caird coinheringaahing

2:49 PM

Q: If we request clarification on a challenge, but the OP has deleted their account, what's the correct course of action?

Cows quack

ask on meta, so that we will also know what to do to any future such cases

caird coinheringaahing

@Cowsquack Ask ^^ on meta, or ask the clarification on the challenge? I'm guessing the former, but just checking

Cows quack

@user56656 why can't you do (~A -> ~A) -> (A -> A)?

yes, the former

user56656

You can it just requires proving (~A -> ~A) which is just as long as proving (A -> A)

Cows quack

~~but you are using LS3 to reach that statement~~ nvm okay I understand now

H.PWiz

2:58 PM

Without a rule like φ -> ~~φ, LS3 seems to be not very useful in proofs

Cows quack

but for the actual challenge, why can you not use φ=¬A and ψ=¬B in (¬φ → ¬ψ) → (ψ → φ)?

oh I see, you cannot use A→¬¬A without proving it first as HP said

caird coinheringaahing

3:11 PM

@Cowsquack Posted, just waiting on NMP :/

user202729

Call it "NmP" please.

> the OP has deleted their account

> highly upvoted and answered

==> ais523

(is there anyone else? I know some users who appears to left the site, but not delete the account)

caird coinheringaahing

@user202729 I know I could probably ask them in here via their new account, but it's more of a general case "What do we do in this scenario?" issue

New Meta Posts

0

Q: How to request clarifications when the challenge poster has left the site?

Recently, I began to attempt to answer this highly upvoted and answered question, before realising that, by taking the length of the input as an input would allow me to greatly reduce my code. However, as whether this is acceptable changes between challenges, I went to comment below the challenge...

discussion challenges clarification

ETHproductions

3:39 PM

@Cowsquack I've had this question since I saw the challenge in the sandbox, didn't want to ask though because I figured I was just missing something obvious

Erik the Outgolfer

3:53 PM

I don't think you can use anything else but the three axioms

Cows quack

and modus ponens

Erik the Outgolfer

modus ponens comes from how → works, it's not really something new

Cows quack

4:17 PM

@user56656 would proving ¬¬A→A or A→¬¬A be sufficient to replace every occurence of ¬¬A with A?

user56656

Could you be a little more precise?

Erik the Outgolfer

@Cowsquack "either this or that" isn't going to work

the former is what you need in this case

user56656

You can't use ¬¬A→A to automatically change every occurence of ¬¬A to A?

Erik the Outgolfer

you can't use A→¬¬A

user56656

but if you do prove ¬¬A→A you may be able to systematically replace every ¬¬A with A.

J. Sallé

4:19 PM

Logic makes my brain hurt.

Cows quack

if I prove either/both of those two, can I simplify an expression like α→(β→¬¬A) into α→(β→A)?

Erik the Outgolfer

yes, ¬¬A→A is what you should use, not A→¬¬A

totallyhuman

Yay, I won ADVENT.EXE!

user56656

@Cowsquack Not in a single step, but you can use the existing rules to do so over several steps.

Cows quack

so how would you introduce it? Would α→(β→¬¬A) to α→(β→(¬¬A→A)) be valid?

H.PWiz

4:24 PM

Which axiom is that?

user56656

@Cowsquack That wouldn't be valid.

(not in a single step anyway)

of course the second thing α→(β→(¬¬A→A)) is a tautology

If you give me a minute I can write a proof getting from α→(β→¬¬A) to α→(β→A) given ¬¬A→A

Cows quack

@H.PWiz I was asking WW how I would introduce a lemma like ¬¬A→A into the proof, using α→(β→¬¬A) as an example statement

H.PWiz

It was mentioned in the comments before (since deleted). But no lemmata allowed, only axioms and modus ponens. Nothing else

user56656

@H.PWiz Out of curiosity how has your proof been going? I thought you had mentioned you were close. I'm eager to see the first answer.

Cows quack

@user56656 thanks

H.PWiz

4:31 PM

@user56656 Not close, I've had a few attempts, but I just feel like I'm running in circles. And when I try to take a step back and think about what really needs to happen, It never looks like I can do it with the axioms. I also tried for a little while to prove A -> ¬¬A as a warm up, but I couldn't do that either. I too am looking forward to the first answer

PhiNotPi

Terrible programming of the day: my university is hosting some sort of programming event, but for a while there was a bug in the registration form that meant only people with unique first names could register.

user56656

@Cowsquack Here is a similar proof:

https://tio.run/##hVRtb5swEP7Or/CQptjagZbkW7dWCpWmTsrUavQDVRJRtjgNEjEI3GRT1t@e3WEokNBUSGA/9zz3Yt@R5WmSPjnFLj4cIp1u@Ozm3/1CMMe5YrObBex/p0sZ6r@Z5DcQJdk6Ei9QEu@Fa1WKd/iuZe0Kw1i49ZLbzP5iz7UtYFcgQ6WaB8aP7diIQaEjLTdS6RANyIhXPIAHQ@nYiGw7V8eiBxR9fEP0YERf@yO19mWFgTAOqo3bJpi8jd2sO@YqflUYL8NVWJmBsDv0oEM8rZLoDb/rveO55bV22uMQnf2KlmFDndVXiRd1ZAmavgjwnoP55fDzC3RJ1BNWUgzrkPvgElOaUF4hTAS2TjsrF6mjLrVme3AtBNSAVy4nhPW4GJ@4oHuYCKCPZ9x4fdGtXBY6TFdhEiv5Whnb45vNL9njXD2@AGuT3FOJPVd0J1ke46kWWmbc1xsNPq4Eu3BYts6jQvImMpkFMF/n@KaOCmlkCiyvhHZ5rCVlv4myJC40LwHjD1QCHzDYNkripQkWQGiKN6cOlA7sW9kEwGYDNvWHgwVNYr90dFY6Oicdn5WOe6T…

H.PWiz

@user56656 For extra clarification, our proofs, in your program should have no lines labelled "Invalid step"?

user56656

Yes they should. My invalid steps there are assumptions I make.

H.PWiz

good good

Cows quack

4:36 PM

@user56656 ah, I see

by the way, I think en.wikipedia.org/wiki/Propositional_calculus might be a good resource to include in your challenge. #Example_1._Simple_axiom_system demonstrates a calculus using the Łukasiewicz axioms and modus ponens as its inference rule

totallyhuman

Wait, it is possible, right..?

user56656

@Cowsquack Link added.

@totallyhuman Any true statement in propositional logic can be proven with the Łukasiewicz system.

I've also done the proof myself. (I actually used lemmata to do this but it doesn't change the validity of the proof)

Cows quack

btw wheat wizard, are you studying pure mathematics or applied mathematics?

user56656

4:52 PM

On paper I am studying pure mathematics. In practice my university doesn't offer a lot of pure mathematics.

My logic courses are actually run by the philosophy department