bvssvni

7 ms·

1.
by bvssvni 2y ago
I tried to get Jonathan Blow engaged in the Rust RFC process to improve productivity for gamedevs. However, he thought it was a better idea to start working on his own language (Jai). When I did some research for the Piston project, I learn
2.
by bvssvni 3y ago
Logic by default does not have a bias toward consistency. The bias is added by people who design and use mathematical languages using logic. It does not mean that the theory you are using is inconsistent. Asking "why do you want to be
3.
by bvssvni 3y ago
Yeah, this is too imprecise. I tried to translate to your terminology, but failed. My system uses "tautological equality" and this allows me to treat them the save way for all tautological congruent operators. Ofc, you can't
4.
by bvssvni 3y ago
I want to reason hypothetically, which is why I don't use syntactic equality. I only use syntactic inequality in a very limited sense, e.g. two symbols `foo'` and `bar'` are symbolic distinct, so one can introduce `sd(foo&#x2
5.
by bvssvni 3y ago
In mathematics, the roof holds up the building, not the foundation. Since humans use mathematics a lot, we design foundations to our specific needs. It is not the building we are worried about, we just want better foundations to create bett
6.
by bvssvni 3y ago
> Does `a^b` mean `a` is provable in all worlds in which `b` is valid, i.e. taken as an axiom in the underlying proof theory, or something like that? Yes. You can also think of it as a function pointer `b -> a`. Unlike lambdas/cl
7.
by bvssvni 3y ago
> Something being random and/or undetermined is not sufficient for it to be like a qubit. You need the linear algebra aspect for the name to be appropriate, IMO. Naming things is hard. Given how constrained Propositional Language is
8.
by bvssvni 3y ago
> Are you saying that Löb's axiom, which states that the provability of "the provability of p implies p" implies the provability of p, necessarily prejudices some implicit assumption of consistency to the meta-language? Ye
9.
by bvssvni 3y ago
I think the most exciting work in mathematics today is in the formal foundations. However, I can also understand mathematicians who are thinking like this: 1. I only need normal congruence 2. I only need perfect information games Under prob
10.
by bvssvni 3y ago
> I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ? yes > I viewed the page you linked, but I don't see anywhere where you describe the altern
11.
by bvssvni 3y ago
I'm implementing it in this project: https://crates.io/crates/hooo
12.
by bvssvni 3y ago
One thing I would like point out with Gödel's incompleteness theorems, is that there are different notions of provability. Gödel uses the notion of "provability" you get from Provability Logic, which is a modal logic where yo
13.
by bvssvni 3y ago
Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?
14.
by bvssvni 3y ago
The foundations of mathematics are all about language design. To answer this question, one must say something about which language a foundation of mathematics is using. For example, Set Theory is formalized in First Order Logic. However, Fi
15.
Let's Abandon the Cogito and Use Type Theory Instead(advancedresearch.github.io)
2 points by bvssvni 5y ago|0 comments
16.
by bvssvni 5y ago
This update changes the PSI implementation (path semantical logic) to use a safe model of path semantical quality. The problem previously was how to handle reflexivity without symbolic distinction (this is beyond IPL - constructive logic).
17.
Prop v0.8 released Propositional theorem proving in Rust (Logic)(old.reddit.com)
3 points by bvssvni 5y ago|1 comments
18.
Joker Calculus(github.com)
2 points by bvssvni 5y ago|0 comments
19.
by bvssvni 8y ago
Link /r/rust thread: https://www.reddit.com/r/rust/comments/9x5uvk/advancedresear...
20.
A linear solver designed to be easy to use with Rust enums(github.com)
4 points by bvssvni 8y ago|1 comments
21.
by bvssvni 8y ago
This is a scripting language I've been working on since 2016. Originally, I did not plan to make a language, but I had a couple weeks available for some project while waiting for Gfx upgrades. It turned out to be so much fun to work on
22.
Dyon 0.36 is released(github.com)
3 points by bvssvni 8y ago|1 comments
23.
by bvssvni 10y ago
This is not just about applying universal basic income, negative tax etc. The algorithm fine tunes the whole economy using a single parameter. People can vote on the inequality level they think is healthy for economy, and the solver guarant
24.
Solving Economic Inequality in MMOs(blog.piston.rs)
5 points by bvssvni 10y ago|1 comments