because the set of all theorems would form a small category where arrows can be either implications or proofs.
It wouldn't work for non-true props included because $\implies$ arrows don't associate when you compose them.
What is formed is a category without associativity axiom also known as a deductive system
I'm not currently encoding that though (yet). I'm sticking mainly to category definitions in my code
A proof is a class such as id_is_unique that inherits (subclasses) proof, which is a type of morphism in $\textbf{TrueProp}$ or $\textbf{Proof}$.
I think the latter is more appropriate because as I observed the arrows of true prop objects might as well be implications so that they are unique. Proofs are more interesting because you could have a large space of them
I.e. one way of proving something and then another way that doesn't appear to be like the first way at a glance. In that case I don't consider them equivalent. But I think type theorists do - something like that
I'm making a CAS that you use to prove things, and when you prove something, it can auto-generate an extension to the source code, you then re-compile and have access to it "statically". But of course you could use whatever proven things you make at runtime just as well.
It's just better to organize the proof in a coding language than some unreadable data format
So that the set of true props is a small set, I take as an "axiom" in the metatheory. It just gets hardcoded in. But I'm not using const everywhere, so things are "hackable". I like that about it. I believe though if you create some usage constraints, and are a smart enough logician (I am not), then you could prove that the system is consistent, complete, etc. All that logic theory jargon.
But why develop another strict formal system, when they exist. I could simply output to other languages.
it wouldn't be simple, but it would be simpler than creating another Lean or Coq
The point of this project is to do extremely fast searches for diagram-chase kind of proofs starting out.
@Shinrin-Yoku not sure to which question you are referring.
> It is well known that SSA is not a valid congruency rule; however if we are given two sides and an angle opposite to the longer side then it becomes valid, how to prove this? Is there a geometric proof? Also is it always the case that it fails if the angle is opposite the shorter side?
I have a seemingly extremely easy problem but I can't seem to find the way to formally prove it...
Suppose I have 2 probability distribution functions on two sets, A and B. Now suppose that I have variables taking up values from each of these probability spaces
how do I prove that my 2 variables are independent?
Intuitively they're obviously independent since the 2 PDFs are completely separate from each other
but I'm not sure if that's enough to count as a "proof"
(I bought limes yesterday, and my home-made orange liqueur is very good, so I have been consuming margaritas tonight---my first impulse is to assume that you know measure theory, and have defined independence in that context. This is probably not right, so it would help to know what you mean by "independent".)
I'm trying to align multi-line equations but the following just prints as a single line: $$\begin{align*} S & = x^2 + 2x &&\text{(note 1)} \\& = x(x + 2) &&\text{(note 2)} \end{align*}$$
You may need to copy out the edit pane and refresh the page and then paste back the edit pane. I sometimes have to do that a few times. Something goes wrong once in a while.
@Shinrin-Yoku You should be trying to understand what the diagrams I posted are showing. Given the angle, the length of the first side and then the possible locations of the second side, you should be able to tell something about the third side.
@Shinrin-Yoku There is that possibility, or maybe it doesn't touch it at all.
Suppose that $\mathfrak B$ is the Borel sigma algebra and $\mu$ is given to be a measure on $\mathfrak B$ with the property that $\mu([0,1])= 2$, then how do I show that $\mu=2\lambda $, where $\lambda$ is the Lebesgue measure?
I was thinking of showing that $\mu$ and $2\lambda$ agree on all closed and bounded intervals and then using sigma finiteness of sigma to show uniqueness of the extension.
If I could show that $\mu [a,a+n]= 2n$ then I think I’ll be able to take it from there.
I’m having difficulty realising value of $\mu$ on a singleton set.
which I believe should be 0 but I don’t know how to prove it yet. [0, 1/2) U[1/2,1)U{1}= [0,1], and then by additivity, I get $2\mu[0,1/2)+\mu\{1\}=2$.
@Koro if a point has positive measure, then translation-invariance implies every point has the same positive measure. can you see that this implies that every infinite set has infinite measure?
Hi @Thor, I figured that out. $\sum_{i=1}^\infty\mu\{r_i\}\le \mu([0,1])$, where $r_i$ is enumeration of rationals in [0,1] and noting that $\mu\{r_i\}=\mu\{r_i+\{0\}\}=\mu(\{0\})$. The series is bounded iff $\mu\{0\}=0$.
@Ajay One nice series to remember is $$\sum_{k=0}^\infty\binom{2k}{k}x^k=(1-4x)^{-1/2}$$
The generating function for the central binomial coefficients, which gives $$\frac{x}{\sqrt{4-x}}=\frac{x}2\sum_{k=0}^\infty\binom{2k}{k}\left(\frac{x}{16}\right)^k$$
One presentation for $G=\Bbb Z\oplus \Bbb Z_2$ is
$$P=\langle a,b\mid b^2, ab=ba\rangle.$$
Note that $H$ is the normal subgroup $Q=\langle a^2b\rangle$; therefore, the quotient is given by $P/Q$, which is
$$P/Q\cong\langle a,b\mid a^2b, b^2, ab=ba\rangle,$$
so we can write $b=a^{-2}$ to get
$$P/Q...
Is this a known problem? Consider a stick of length 100. At each step choose an integer break point uniformly along the stick (it could be right at one of the ends), break the stick and remove the right hand part. We store all the parts that have been removed. What is the expected size of the largest part we have removed?
I had such a great time not understanding Dirac notation. It was wild to me. at some point, probably easy linear algerba became too complicated or my eyes.
But sadly, we didnt do it rigorosly at all, at some point, my professor gave up and just started bringing stuff from his research group about one dimensional lattice things
The progression of weirdness goes roughly as: spin of a single particle, position of single particle / spin of many particles, position of many particles
Historically presentations of QM start at the “position of single particle” portion, aka the ordinary Schrodinger equation
I prefer to start with the first point aka the Stern-Gerlach experiment
But the last point aka QFT is where things become wacky
I dont think you can convince me of doing any more quantum mechanic than i should in my college. so i am not doing QFT. But i dont know, i feel it wasnt my fault, i felt it was more the lecture was bad. i think i am an okay student if the lecture is not bad, i can do good.
I say it isn't. It's high school matrix multiplication. The facts that I could write down $A^\top A$ faster than a high school student and know its eigenvalues immediately ... might be helpful.
Well, reading the info for the linear-algebra tag, matrices seem to fit. It is definitely very basic, but so are a lot of supposed analysis questions. Gotta ignore the chaff.
they have an elementary number theory tag to sort out the elementary questions there, perhaps they need more elementary tags
Oh, I was not debating the tag. I do modify tags on almost every question I bother to look at, though. No one knows what complex geometry means, and sometimes differential geometry isn’t much better.
