Logic - 2017-12-14 (page 1 of 3)

David Reed

02:13

hi there

popped in about 5 sec before you. How are you?

user21820

Hello! Haha I am just popping in, and need to go soon.

David Reed

no worries

I'm like 99% certain I'm getting a 3d printer for christmas

do you happen to have one?

Just curious as to where the best site to download other's schems would be

Also, please advise as to where I can find the quining-free proper proof of the diagonal lemma we were discussing the other night. I'm curious to review it

David Reed

02:33

@user21820 I had meant to ping you in the above.

user21820

02:54

No I don't have a 3d printer.

@DavidReed That is why I did not use the diagonal lemma at all in my linked post on the right.

What I meant in that comment last time was that there is no need to show that we can create a quine in the programming language we chose.

I actually thought you knew the proper proof of the diagonal lemma, since your book has it, and we discussed it before. Just apply any fixed-point combinator to the 1-propositional-parameter sentence f = ( x ↦ ¬⬜x ).

We essentially want ( x ↦ f(x(x)) ) ( x ↦ f(x(x)) ).

David Reed

@user21820 I interpret the proof in my book as using self-reference

Could you recommend a txt that takes the computability approach to these theorems?

Given your fondness of it I would very much like to engage in it myself

user21820

Well what I saw in your book does not have any self-reference. The Godel sentence does not actually refer to itself. Only from the outside (namely in the meta-system) do we see that it apparently does.

David Reed

Yes that's what I mean

concretely it is just a statement about arithmetic

but in the abstract, in the "meta-system" it effectively refers to itself

user21820

But that's very different from self-reference or quining. Compare the following:

> "This is unprovable".

> G = "code(G) is unprovable", where code(P) is a natural number such that "code(P) is unprovable" is true in the naturals iff P is unprovable.

The first can be said to be self-referential. The second cannot, because there is this pesky "code".

David Reed

03:11

I think the breakdown here is we just have different definitions/notions of the concept of "self-reference"

user21820

But I think it's crucial to maintain the distinction, because they are actually qualitatively different. Otherwise consider:

David Reed

I consider the 2nd to be self-referential as well

user21820

> "This is false".

No think about the example I just gave.

It is self-referential, and impossible to construct.

At least, impossible in classical logic.

David Reed

one moment..phone call

@user21820 Back. Sry about that

user21820

No problem.

David Reed

03:18

give me a moment here to review what you've said

Would you consider yourself a constructivist?

If I were to give an existence proof via contradiction would you find that acceptable?

I'm speaking in general here, not necessarily this particular context

I don't disagree that the first and third examples you have given are self-referential

I do believe, based on my personal notion of what would be considered self-referential, that the 2nd one you gave is self-referential as well

user21820

@DavidReed It clearly depends on the system your proof is in. If your proof is in a system that I believe to be meaningful, then what it uses is irrelevant. But if your proof is in a system I do not believe to be meaningful, then I would have to see what deductive rules/axioms you used.

To be more philosophically precise, you ask whether given a justification that "if A is true then contradiction" I would accept that it justifies "A is false".

David Reed

You strike me, based on the totality of our conversations, to be very much a constructivist, or at the least you lean that way relative to the average mathematician

user21820

My answer (consistent with what I just said) is that it depends on whether A is a meaningful sentence with a true/false value.

David Reed

Let me link you as to what I mean by a constructivist. It doesn't necessarily need to have anything to do with proofs in a formal system

Constructivism (mathematics)

In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. In standard mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. This proof by contradiction is not constructively valid. The constructive viewpoint involves a verificational interpretation of the existential quantifier, which is at odds with its classical interpretation. There are many forms of constructivism...

user21820

If you can justify that it is such a sentence, then quite automatically I would have no choice but to accept the reasoning. But if you cannot justify that A is a meaningful true/false sentence, then I reject the reasoning.

I have read that before. It's unrelated.

People keep conflating constructivism with skepticism of silly assumptions.

David Reed

03:29

phone again. quite sry. Perhaps a more concrete example would help me to understand your position better. I shall think of one to pose to you

user21820

Sure.

But you should first read (if you haven't):

6

A: Is Godel's modified liar an illogical statement?

Your question has two main facets. The first is that you did not grasp the way logic does not fall to the liar paradoxes. The second is that there are deeper reasons as to why we have such apparently innocuous sentences in natural language that seem to defy assimilation into formal logic systems....

David Reed

Concrete example: The proof of the mean value theorem is an existence proof. It tells you that something exists but gives you no knowledge as how to find it.

The proof of the Chinese Remainder Theorem is another existence proof. In this instance, the solution to the system of congruences is explicitly constructed.

Do you reject the first ?

user21820

Do you know the proof of MVT? You would simply have to go through it and see whether at any point you invoke LEM on a sentence that cannot be justified to have a truth value.

David Reed

So the MVT is arguably the single most important theorem in analysis. I do know the proof of it

user21820

So you know where LEM is used. Can you justify it?

David Reed

03:42

Reading that above, on classical logic only being allowed to refer to objects that exist. What do you make of syllogisms having a premise such as "all unicorns are horses"?

I'm not familiar with the acronym LEM.

user21820

Law of Excluded Middle.

David Reed

Ah

user21820

It's what justifies proof by contradiction.

Because if A can only be true or false, and from "A is true" you can deduce a false sentence, then the only possibility is that A is false.

David Reed

Yes a constructivist would reject LEM. It sounds like you actually do not wholly object to its use, but rather it depends on the context. Is that a fair characterization?

In particular, it seems like you are saying that sometimes one tries to apply LEM to statements that don't have a truth value. I would be curious of an example.

user21820

Yes. Essentially LEM is the only non-constructive thing in classical logic, because you can recover proof by contradiction from LEM and disjunction elimination. I accept LEM for sentences that really have boolean truth value. I do have my own particular idea of what those are, but I am open to people convincing me of the boolean valuedness of other sentences.

@DavidReed That's why I said you should first read the linked post. It has an explicit example.

David Reed

03:47

I stopped reading to ask you the existential import question on the unicorns :)

As it struck me that unicorns don't exist, but the premise "all unicorns are horses" would be acceptable as a premise in a syllogism

In other words, I got sidetracked :) But I will finish reading now

user21820

Lol. Yes it should be fine by standard interpretation of that as a restricted universal statement where "unicorn" is somehow defined precisely enough.

@DavidReed You can skip straight to the example, Quine's paradox, if you wish.

David Reed

"In classical logic one is only allowed to refer to objects that exist" in particular was what threw me. Thanks, I was just fixing to ask explicitly where it was located

What do you make of the argument that it indirectly uses self-reference

It seems that some would argue that, and that would be the exact type of self-reference I would consider to be used in the diagonal lemma

user21820

@DavidReed Well "objects" in that line was intended to refer to any entities, physical or not, including mental concepts. Even contradictory or imaginary concepts (like "unicorn") are objects, but they remain as mere concepts without instantiation.

David Reed

Interesting example regarding LEM application. I don't believe that they tend to be very prevalent in mathematics itself. So in general I would actually not consider you to be a constructivist.

ah i see

user21820

@DavidReed I agree that Quine's construction is exactly the same as in the fixed-point combinator. But there is no real self-reference. Just run Quine's construction and see. It says you take this string (it does not matter what its contents are) and then you prepend its quotation, and then you get a false sentence.

David Reed

03:57

It is becoming a pattern to me that we frequently argue endlessly only to discover we actually hold the same opinion on an issue lol

user21820

Nowhere does it say anything literally about itself. It is only you who make the connection via the semantic boosting through "is a false sentence".

Namely, before that last part you just have some string preceded by its quotation.

Only when you attempt to obtain its semantic truth value does it become the same as the original. So there is a crucial gap.

But did you understand the error in the reasoning, and my resolution of that paradox? It is an explicit example that does not obey LEM.

David Reed

Yes. Mentioned above in "Interesting example of LEM application..."

I can't think of ever coming across that in a mathematical proof

user21820

It does not because it is forbidden in first-order logic.

It is only possible in a looser system such as with a 3-valued logic.

David Reed

Never studied 3-valued logic.

If its more expressive than FOL I would probably not be inclined to embrace it

user21820

I invented it as part of my own foundational system, and then found that Kleene already defined it before. Basically a statement can be either true or false or null/undefined/unknown.

The semantics are what you expect (hence why we all reinvent the wheel).

Namely ( A or B ) is true as long as either A or B is true, even if the other is null.

And ( A and B ) is false if either A or B is false, even if the other is null.

David Reed

04:04

blech

iffy for me

user21820

3-valued logic nicely captures real logic circuits with pull-up, pull-down, and open connection.

You like logic circuits, didn't you?

David Reed

I do,

I never came across anything that I would need that for

Although admittedly by CPU was quite simple

my*

LastIronStar

Hi @user21820 @DavidReed

David Reed

hi there!

user21820

Many simple logic circuit programs use such non-classical logic to evaluate the circuit state.

Such as Logisim.

David Reed

04:06

don't remember that being relative to RAM either

concrete example?

No not a program I mean

LastIronStar

@user21820 How powerful is finite automata?

David Reed

Ill Wikipedia and see what comes up

user21820

@LastIronStar Can only recognize regular expressions. Cannot be used to accept only binary strings with an equal number of zeros and ones, and reject all the rest.

@DavidReed Example of what?

David Reed

got it

nvm

reading wikipedias three-state logic article as applied to electrical engineering

user21820

Ah I see. Didn't know you wanted a reference.

For logics actually there is a 4th value often used, for short-circuit!

LastIronStar

04:09

@user21820 lol i totally forgot this, thanks

David Reed

It explicitly warns that tri-state logic should not be confused with three-valued logic

user21820

But for logic used in reasoning, we do not have anything like short-circuit.

@DavidReed That line in Wikipedia is either misleading or wrong.

David Reed

This is not really an application of logic in the classical since. Impedance is difficult to explain as it requires going into complex numbers, but it can effectively be thought of as meaning "high-resistance"

Basically meaning the output is a total absence of an output

doesn't really fit into any notion of actual reasoning

user21820

@DavidReed That is exactly what "null" would represent.

Hence the semantics I mentioned above.

David Reed

Yes, but requires no concept really of true or false in this context

user21820

04:13

True is pull-up, and false is pull-down.

Of course it's not a matter of truth, just truth values.

David Reed

in some contexts in digital logic, 1=T, 0 = False actually translates to true or false. In others it really doesnt

Adders would be an example

Yes, so I can embrace this specific application of tri-state logic without having to really embrace its application in reasoning

user21820

If we stick to modern computing, even binary words can be understood via truth values. A bit is true iff that bit's place-value is added.

And if you're familiar with the efficient addition circuit, it's even more strongly related.

If you're not, it's a fun puzzle to figure out how to minimize the number of gate delays in adding n-bit binary numbers.

David Reed

There are several different addition circuits I am familiar with. None of them require interpreting any truth value in the inputs/outputs of the requisitite logic circuits

user21820

What is the asymptotic complexity of the number of gate delays?

David Reed

No idea. How is this relevant to assigning truth values to bits used in these circuits?

user21820

04:19

The optimal solution, when I found it, required me to think in terms of truth values of the bits exactly as I described above.

David Reed

hrm. Don't really follow.

I'm trying to remember the name of the addition circuit I found to be most efficient

was something carry on adder

give me a moment

user21820

If you want to try this puzzle, I won't tell you the solution yet, but if you want to see my solution, I do have the circuit schematics.

David Reed

carry look ahead adder

that was it

and it appears to be the most efficient in terms of prop delay as well

I see no reason to think of it in terms of truth values

but you and I may simply reason differently

Or you may have come across a more-efficient one?

Circuit schematics are difficult to read. If you have a truth table definition of it's components and it's algebraic expression absolutely! Would love to see it

user21820

Mine is log-depth.

The one you're referring to is:

Lookahead carry unit

A lookahead carry unit (LCU) is a logical unit in digital circuit design used to decrease calculation time in adder units and used in conjunction with carry look-ahead adders (CLAs). == 4-bit adder == A single 4-bit CLA is shown below: == 16-bit adder == By combining four 4-bit CLAs, a 16-bit adder can be created but additional logic is needed in the form of an LCU. The LCU accepts the group propagate ( P G {\displaystyle P_{G}} ) and group generate ( G ...

Which also should be log-depth, just more convoluted.

Heheh.

David Reed

Still

would love to see it

but not as a circuit diagram :(

user21820

04:33

This is the unit.

David Reed

ah that's not so bad

user21820

It is put together as follows:

David Reed

that's horrific

user21820

It's the same unit just repeated in a perfect binary tree.

So as long as you understand the unit, you understand the whole thing.

That's why it's a bit 'neater' than the carry look ahead adder.

The inputs are the squares, and the outputs are circles.

Those are copied from Logisim.

On the left you see a triple for each bit, 2 inputs and 1 output.

David Reed

If neater translates to equally fast and more space/cost efficient I would advise you to sell it

I would be surprised though, given the billions in research that has gone into this sort of thing already

In either event I applaude your intellectual curiousity on the subject. That is, doing it "for fun"

user21820

04:37

Cost-efficient is always less neat, because you can build the circuitry using CMOS technology directly into the circuit, and so there are various things one could do that are more efficient than just using ordinary 2-input gates like I did.

David Reed

I'm the same way and I rarely come across people with that personality

user21820

The advantage of my design is that it's totally modular down to 1 bit.

@DavidReed Haha not many are like that. Most just want to get the grades and be done with it.

David Reed

I assumed yours as being built from MOSFETS

user21820

I didn't actually build it, but I simulated it in Logisim.

Intended to use MOSFETS, yes.

David Reed

Yes, I know you didn't actually build it :) That would be insane given the complex process it entails (sun lamps etc)

At best ppl buy programmable logic circuits these days

user21820

04:41

@DavidReed Actually it would be easy to 'build' it on a bread-board, just that you would need a couple of them.

Of course you need to buy those chips with the gates.

David Reed

I think they actually prefer to build things out of NAND and NOR gates in terms of efficiency

user21820

Not true. That is many years outdated.

David Reed

Believe I recall coming across that in one of my texts

user21820

Now CMOS gates are equally efficient whether it is NAND or NOR or AND or OR.

David Reed

Hrm. I will see if I can come across that and see the year it was published. None of mine were THAT old I think

user21820

04:44

And as I said earlier they no longer just use 2-input gates in the internal CMOS circuitry.

David Reed

I would be surprised if the modern addition circuits used tri-state logic gates

based purely on the Wikipedia article I read

I happen to be friends with an EE, I'll ask him

user21820

They don't use tri-state logic gates. I didn't say that.

Wait I'm not sure they don't, but I didn't say that.

David Reed

I know

user21820

Oh.

But at least I can show you that CMOS NOT gate is not done using NAND or NOR:

David Reed

I just meant in terms of circuits that don't use them, whether there would be a preference for NAND over AND in terms of space/efficiency

CMOS not gate is just an inverter

I didn't mean they didn't use not gates

I meant they would rather build circuits out of NOT, NAND, and NOR instead of NOT,AND,OR

user21820

04:49

@DavidReed Modern CPUs are not designed in terms of gates anymore.

David Reed

what do you mean by "designed"?

user21820

They just put some formal specification of the CPU properties, and then the designing software will compute what it thinks is the best actual physical circuit, which may not look like the ordinary logic gates.

David Reed

Ok yes

I thought you meant that they didn't actually use gates anymore

user21820

In particular, you would expect to see lots of those two physical components as you see in the NOT gate, but you won't see NANDs or NORs or even ANDs or ORs.

Not usually, at least.

I don't think those transistors are called gates anyway.

David Reed

transistors are never referred to as gates

user21820

04:53

Then arguably there's no longer any gates in the design of modern CPUs.

David Reed

transistors are the building blocks of gates, as your above depiction of the inverter shows

user21820

The designer does not think in terms of gates, and the final product is not decomposable into gates.

David Reed

you build gates out of transistors, then zoom out and build things out of gates, then zoom out again and build things out of these bigger things, then zoom out again

that's the general principle behind it

user21820

No as I said that's no longer true.

David Reed

Nobody could look at a transistor schematic of a circuit and be able to understand what it does

user21820

04:55

The designing software does not use gates to implement the specified design.

That used to be true in the early days, which is why some spacecraft had loads of NOR gates.

David Reed

That is a fundamental design principle in general, and I can say with absolute certainty it has not been disregarded altogether

I agree that they have software find the most efficient design for certain elements of a circuit

I want to see the year my text was published that mentioned NAND/NOR was more efficient

one moment

user21820

As I said, the final product is not decomposable into gates. So whether or not it is effective to use gates in an intermediate step, it is not the most efficient at all, and not the way it is done today.

David Reed

That is feasible for certain subcomponents of an entire system, I would be surprised if that was the case universally

I shall ask my EE friend

As of 2007, NAND/NOR was preferred. I grant you that a lot has happened since then :)

user21820

Preferred by whom?

I do not agree. Many textbooks are outdated, sometimes just because they don't want to confuse students.

Secret

@user21820 I have used your exact code in the online C++, and indeed ab= TT, TF give me errors

user21820

05:03

@Secret I replied to you earlier. Quote me.

David Reed

According to Wikipedia: De Morgan's theorem is most commonly used to implement logic gates as combinations of only NAND gates, or as combinations of only NOR gates, for economic reasons.

user21820

@DavidReed That's stupid. Wikipedia is wrong.

Trust me, I know enough to tell you that it used to be true some decades ago but is totally false now.

David Reed

However, it also says the preferred now is AOI and OAI gates

user21820

I dispute the "for economic reasons", not the whole sentence.

David Reed

It also says active research is underway in molecular logic gates, which suggests that gates are not completely obsolete

You are asking me to take your word over a website subjected to peer-review on a daily basis and a textbook of mine written by two people with Ph.D's in electrical engineering

Please don't take my hesitance offensively. If you could point me to something from a reliable authority believe me when I tell you I am very open minded to being wrong

user21820

05:06

@DavidReed Yes. If you find that hard to swallow, then just forgot this topic. I can easily show you tons of serious errors in both Wikipedia and textbooks.

It's difficult to find this kind of information. If I could, I would provide it to you.

Secret

@user21820 So I don't know why I did not get the All valid for ab=TT,TF,FT,FF as you would expect

David Reed

I don't doubt it, I find errors in texts all the time as well. In this instance though two unrelated sources are in agreement

I will ask my EE friend, and we can table the discussion until then :)

user21820

Sure.

Ask him if he knows the whole process from Verilog to CPU chip.

That would answer most of our questions.

@Secret Quote my response to your last message explaining why you got an error.

Secret

14 hours ago, by user21820

@Secret You too didn't read the output.

But now I have all 4 outputs presented

user21820

You have not read the output of the program itself.

14 hours ago, by user21820

It tells you which line is false. And that line tells you why it is invalid.

Doesn't it say something like "Line XXX: False assertion!"?

Secret

05:13

What do you mean????
$g++ -o main *.cpp
$main
a=true
b=true
Line 16: Reached
Line 31: False assertion!

$g++ -o main *.cpp
$main
a=true
b=false
Line 16: Reached
Line 31: False assertion!

$g++ -o main *.cpp
$main
a=false
b=true
Line 16: Reached
Valid for chosen inputs!

$g++ -o main *.cpp
$main
a=false
b=false
Line 16: Reached
Line 19: Reached
Valid for chosen inputs!

#include <iostream>

using namespace std;

#define assert(p) { if(!p) { printf("Line %d: False assertion!\n",__LINE__); return 0; } }
#define trace { printf("Line %d: Reached\n",__LINE__); }
#include<stdio.h>
bool imp(bool p,bool q) { return (p?q:true); }
void input(bool &p) { int t; scanf("%d",&t); p=t; }
int main()
{
bool a,b;
a=false; b=false;
printf("a=%s\n", a ? "true" : "false");
printf("b=%s\n", b ? "true" : "false");
trace;
if( !b && imp(a,b) )
{
trace;
if( a )
{
trace;
assert(a);
assert(imp(a,b));

where I use the line a=false; b=false and change the bool for each case; because stdin is not working for me

user21820

Just read the output. In your version, it says:

> Line 31: False assertion!

Did you actually read line 31 in your program?

Secret

assert(!a); // Invalid, unlike the above assertions. Find an input that fails it!

there are two "assert(!a)" in your raw program

user21820

So? It tells you that it is invalid, so why do you expect it to be valid??

Compare against the original program that I said corresponded to the original proof.

As I told LastIronStar, I did not intend to trick anyone, but somehow I tricked both of you...

16 hours ago, by user21820

So you've to comment/delete that line to get the one for the original proof.

Secret

I thought your want us to to show the program you posted as is is valid, which is why I am very confused when I noticed your pseudocode does not contain line 31

user21820

You found an input that fails that line, exactly as I asked for in the program. You did not find any input that fails the other assertions, which should have been enough for you to understand the validity of those assertions.

Does it make sense now? I didn't say that my full working code was a valid proof.

Secret

05:20

> I didn't say that my full working code was a valid proof.

Right, I see now. somehow I missed that part of the instructions because I am mostly in h bar yesterday when you and Lastironstar talked about the program

user21820

So do you understand exactly why the proof as program is valid?

Why the valid assertions are valid?

The trace is there to assist you in tracing what gets executed.

@DavidReed: Aha I found a couple other Wikipedia articles that support what I said, but well since Wikipedia is not reliable you'd have to verify them yourself somehow. =)

NOR logic

A NOR gate is a logic gate which gives a positive output only when both inputs are negative. Like NAND gates, NOR gates are so-called "universal gates" that can be combined to form any other kind of logic gate. For example, the first embedded system, Apollo Guidance Computer, was built exclusively from NOR gates, about 5,600 in total for the later versions. Today, integrated circuits are not constructed exclusively from a single type of gate. Instead, EDA tools are used to convert the description of a logical circuit to a netlist of complex gates (standard cells) or transistors (full custom approach...

> For example, the first embedded system, Apollo Guidance Computer, was built exclusively from NOR gates, about 5,600 in total for the later versions. Today, integrated circuits are not constructed exclusively from a single type of gate. Instead, EDA tools are used to convert the description of a logical circuit to a netlist of complex gates (standard cells) or transistors (full custom approach).

It links to the following:

Netlist

In electronic design, a netlist is a description of the connectivity of an electronic circuit. In its simplest form, a netlist consists of a list of the electronic components in a circuit and a list of the nodes they are connected to. A network (net) is a collection of two or more interconnected components. The structure, complexity and representation of netlists can vary considerably, but the fundamental purpose of every netlist is to convey connectivity information. Netlists usually provide nothing more than instances, nodes, and perhaps some attributes of the components involved. If they express...

Secret

yup, ab=FF is the only one that made !b and a=>b true, but then a is not satisfied thus the code in the 2nd if doe not get executed. For all other ab pairs, the "!b and a=>b" gives false thus it never entered the if codes and thus go straight through.

Therefore assert(a);
assert(imp(a,b));
assert(b);
assert(!b);
assert(false); is never being touched by the program for all four pairs ab

user21820

Full custom

Full-custom design is a methodology for designing integrated circuits by specifying the layout of each individual transistor and the interconnections between them. Alternatives to full-custom design include various forms of semi-custom design, such as the repetition of small transistor subcircuits; one such methodology is the use of standard cell libraries (standard cell libraries are themselves designed using full-custom design techniques). Full-custom design potentially maximizes the performance of the chip, and minimizes its area, but is extremely labor-intensive to implement. Full-custom design...

@Secret Correct!

So it holds that every assertion made is true.

David Reed

the exclusively in "constructed exclusively" is where I had initially differed with you

Secret

@user21820 so uh, if the program never checked some of the asserts, we just default them to true in classical logic?

David Reed

05:26

I took no exception to the fact that large parts of a circuit would be gate-independent

I will read the rest of what you've put up really quick. One moment

user21820

@DavidReed If that's the only difference, then it really comes down to whether the Full custom approach is the dominant approach or not.

Secret

cause if it is in 3-valued logic, those unchecked asserts will be null I think

David Reed

Full-custom design potentially maximizes the performance of the chip, and minimizes its area, but is extremely labor-intensive to implement. Full-custom design is limited to ICs that are to be fabricated in extremely high volumes, notably certain microprocessors and a small number of ASICs.

That being said, even if it were dominant, I would not have disagreed with that

user21820

The citation is 1999.

David Reed

I simply refute the notion that gates are obsolete

user21820

05:29

Let me just clarify what I said. I am not saying anything about intermediate representations, which the software might use, which may be build using gates.

However, they are not actually used anymore in both the human design phase and the machine chip construction phase.

I said this much earlier, but I think you missed it.

David Reed

That the end result of certain elements of an IC may not have any gates present in it I am completely willing to believe

Secret

@user21820 Or maybe I should ask this way: When the program did not ran through the asserts that are in the code, do they actually exists as part of the argument?

David Reed

DRAM uses not gates to store a state

to my knowledge this is still the case

user21820

@Secret As I instructed, have you gone through the following?

16 hours ago, by user21820

Based on this, check that what I said in the three comments starting here are correct.

Secret

@user21820 Yes, I deleted the whole block of if (a), and it gives me no errors, but does that means the assertions in the if(a) never exists in the perspective of the proof when they are inside the code?

David Reed

05:38

SRAM*

user21820

@DavidReed DRAM uses memory cells, each of which is a single capacitor and a transistor. This is not a gate, not to say not gate. I'm not 100% sure what DDR3 RAM uses, but it's bound to be the same, because it's the most space efficient.

David Reed

Yes, I just corrected myself to SRAM :)

I have always gotten those two mixed up in terms of implementation

SRAM is faster but more expensive. On a comp tends to be used primarily in CPU for registers and the like

user21820

SRAM is like in USB drives, and again do not use NOT gates. The memory cells are still like capacitors, just that this time it's in a potential well so deep that the electrons can't get in or out without hot injection.

David Reed

negative

SRAM uses two inverters plugged into each other to store a state

I shall double check to make sure this hasn't changed

user21820

@DavidReed CPUs do not use SRAM for registers. They use flip-flops.

David Reed

05:42

flip-flops to my recollection are the design principle behind SRAM

let me double check, as mentioned has been nearly a decade since I went through this stuff :)

Wikipedia : Static random-access memory (static RAM or SRAM) is a type of semiconductor memory that uses bistable latching circuitry (flip-flop) to store each bit

user21820

There are many different kinds of flip-flops.

I should have been more precise earlier.

But anyway, just look at the circuit schematics for the SRAM on that Wikipedia page.

They are not just two NOT gates joined together.

Similar, but not the same.

David Reed

yes it appears I was remembering incorrectly

NOR gates

not inverters

user21820

That's definitely false.

A NOR gate has 4 transistors.

Join 2 and you get 8 transistors.

David Reed

An SR latch, constructed from a pair of cross-coupled

won't paste

in any event, thinking of it in terms of gates doesn't really help you understand how it works

user21820

I think we should forget this off-topic discussion, since you doubt practically everything I say, and I think it's not really worth my time to argue with you about non-logic topics.

David Reed

05:45

you have to think in terms of voltage

Actually I have just acknowledged being wrong about the inverters

ACTUALLY WAS NOT WRONG!

A typical SRAM cell is made up of six MOSFETs. Each bit in an SRAM is stored on four transistors (M1, M2, M3, M4) that form two cross-coupled inverters

inverter = not gate

but yes, perfectly happy to retable the discussion.

user21820

4 mins ago, by user21820

They are not just two NOT gates joined together.

4 mins ago, by user21820

Similar, but not the same.

I don't like calling 1+1+ε the same as 2. That's all. Let us get back to logic.

David Reed

ok :)

user21820

@Secret As I said, we call a proof valid iff every sentence is true in its context. When interpreted in program form, this means that it is valid iff every assertion made passes.

You did step (1), but did you do step (2)?

20 hours ago, by user21820

@LastIronStar Well there are 3 steps you can do to convince yourself. (1) Run the program I wrote and test all possible inputs and check that it has no assertion error in all cases. This establishes that the proof is valid according to my definition, because every sentence is true in its context. (2) Delete all the assert statements in the program, and add them one at a time in order. Convince yourself that each one can be safely added without possibility of assertion error. If you get stuck reread:

You have to do it one assertion at a time in the order given.

Because that is the easiest way to understand why the final assertion can be safely made.

David Reed

@Secret Hey! Nice to see you. Didn't notice you drop in. Was it you that invited me to chem chat?

user21820

You cannot just say, I ran the program on all possible inputs and it passed. You must be able to reason it out without running.

Then you can use that exact same reasoning to understand the original proof.

That is why you can't really say that the assertions don't exist when they are not executed.

They are there, just not executed, and them being there makes it easier to understand why the final assertion is valid.

@Secret: Do you get it?

Secret

05:56

@user21820 This sounds quite philosophical.I think I need some time to digest that...

user21820

Uh the point is that if you could reason that the final assertion was safe to make, you could just get straight there.

The proof by contradiction is merely used to show without testing all cases that it must be valid.

See, the 1st and 2nd and 4th assertions are obviously safe. The 3rd follows from the 1st and 2nd being safe and the definition of imp.

You can ignore the "assert(false);" if you wish. The point is that the innermost assertions are clearly all safe.

David Reed

Alright, got to go. @user21820 Thank you for the enthusiastic discussion. Very enjoyable chatting with you as always. Until next time.

user21820

But they assert contradictory things. So that is why we can conclude that the final "assert(!a)" is safe.

@DavidReed Sure take care and see you!

@Secret: Let me put it another way, the whole goal of logic is to find a finite collection of rules that allow us to make only true assertions in their context.

It is true that you can in propositional logic just test all possible truth values for the propositions involved to determine what is a true assertion.

But it is unwieldy and no longer possible for first-order logic.

So it is not enough that you can conclude in this one example that the final assertion is safe. You must be able to reason correctly in general. That is why we break it down into smaller steps, even involving assertions in subcontexts.

It turns out that there is a finite collection of rules that will be not only able to justify these smaller steps, but also able to deduce other true assertions in general, in a complete sense. A version of such a rule collection is given in Chapters 6−7 of forallx.

Secret

06:12

I am still at page 6 and I think I overthink about thexercise thus I am currently a bit stuck

Secret

06:36

@DavidReed yeah, cause I moved the chemistry discussion to it

Secret

08:02

1. Socrates is a man.
2. All men are carrots.
3. So: Therefore, Socrates is a carrot.

My attempt: assert 1 is true and assert 2 is true. Then if 3 is false, then contradicts with 2. Hence the argument is valid

1. Abe Lincoln was either born in Illinois or he was once president.
2. Abe Lincoln was never president.
So: Abe Lincoln was born in Illinois.

My attempt: assert 1 is true and assert 2 is true. Then if 3 is false, then 1 and 2 will be a contradiction

1. If I pull the trigger, Abe Lincoln will die.
2. I do not pull the trigger.
So: Abe Lincoln will not die.

My attempt: assert 1 is true and assert 2 is true. Then if 3 is false, there is nothing stopping Licoln to die without contradicting 1 and 2 (bool(pull the trigger)=false, then 1 is true regardless of whether "Abe Lincoln will die"=true, false)

1. If the world were to end today, then I would not need to get up tomorrow morning.
2. I will need to get up tomorrow morning.
So: The world will not end today.

MY attempt: Ok this is the confusing one: How will get up tomorrow morning or its negation had anything to do with 2?

1. Joe is now 19 years old.
2. Joe is now 87 years old.
3. So: Bob is now 20 years old.
My attempt: The truth value of 3 should not have any interaction with 1 or 2 since nothing is said about Bob in 1 or 2. Hence the argument is invalid?

So uh, if I understood correctly, to check whether an argument is valid is to check if we have the conclusion true or false, whether they will lead to a contradiction with the premises

if the premises can still be true regardless of the truth value of the conclusion, then the argument has to be invalid as it will mean the conclusion does not depend on the truth value of the premises

user21820

10:40

@Secret No this is wrong. You don't check if the conclusion is true or false.

Firstly, do you accept the validity (as I defined it) of the example proof I gave?

Secondly, forallx defines that an argument of the conventional form is valid iff the conclusion must be true whenever the premises are true.

It is what the author intended, even if it is not what you interpreted his definition to mean.

More precisely, we can understand the conventional argument form properly by translating it to my form.

The following conventional argument:

> A. (Premise)
> B. (Premise)
> ...
> C. (Premise)
> ...
> D. (Conclusion)

should be interpreted as:

If A and B and ... and C:
  ...
  D.

Nothing more and nothing less.

@Secret: So your attempts are incorrect because validity of an argument has nothing to do with contradiction. It is solely a matter of whether you can justify each sentence as true in its context (after translating as I described above). If you cannot, it is invalid, regardless of whether the conclusion is always true!

LastIronStar

10:58

Hi folks

user21820

Hello!

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic